/LMAR=0/FONT#0=BASL30/FONT#1=FIX30



␈↓ α,␈↓␈α?␈α'EQUIVALENCE AND INEQUIVALENCE OF INSTANCES OF FORMULAS

␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α9by

␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α/Hanan Samet










␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α∪Abstract


␈↓ α,␈↓An␈α∞algorithm␈α∂is␈α∞presented␈α∞for␈α∂determining␈α∞whether␈α∞or␈α∂not␈α∞two␈α∞instances␈α∂of␈α∞formulas␈α∂are␈α∞equal
␈↓ α,␈↓based␈αon␈α
previous␈αequality␈αand␈α
inequality␈αdeclarations.␈α The␈α
equality␈αdetermination␈α
algorithm␈αis
␈↓ α,␈↓shown␈αto␈αbe␈α
almost␈αlinear,␈αon␈αthe␈α
average,␈αalong␈αwith␈αa␈α
completeness␈αproof.␈α The␈αmaximum␈α
space
␈↓ α,␈↓requirement for the equality data base is also discussed.



␈↓ α,␈↓I.  INTRODUCTION

␈↓ α,␈↓We␈α∞are␈α∂interested␈α∞in␈α∞a␈α∂system␈α∞to␈α∞handle␈α∂equality␈α∞operations␈α∞based␈α∂on␈α∞known␈α∂equivalences␈α∞and
␈↓ α,␈↓inequivalences␈αof␈αinstances␈αof␈αformulas.␈α Some␈αof␈αthe␈αrequests␈αwhich␈αwe␈αwould␈αlike␈αto␈αbe␈αable␈αto
␈↓ α,␈↓respond to are:

␈↓ α,␈↓1.  Are two items known to be equal?
␈↓ α,␈↓2.  Are two items known to be unequal?
␈↓ α,␈↓3.  Is it impossible to determine if two items are equal or not?
␈↓ α,␈↓4.  Update the data base to include an additional equality.
␈↓ α,␈↓5.  Update the data base to include an additional inequality.
␈↓ α,␈↓6.  Does the inequality of two items lead to a contradiction (i.e.
␈↓ α,␈↓    an implied equality)?
␈↓ α,␈↓7.  Does the equality of two items lead to a contradiction (i.e.
␈↓ α,␈↓    an implied inequality)?
␈↓ α,␈↓8.  The results of equality tests should be independent of the
␈↓ α,␈↓    order in which the equality pairs are processed.

␈↓ α,␈↓A few examples of the type of requests made to the system are given
␈↓ α,␈↓below:

␈↓ α,␈↓Ex. 1:  Given:  a = b
␈↓ α,␈↓                c = d
␈↓ α,␈↓                b = c
␈↓ α,␈↓        Derive: g(a) = g(d)

␈↓ α,␈↓Ex. 2:  Given:  g(b) = f(a)
␈↓ α,␈↓                g(c) = f(b)
␈↓ α,␈↓                a = b
␈↓ α,␈↓                c = d
␈↓ α,␈↓        Derive: g(a) = g(d)

␈↓ α,␈↓Ex. 3:  Given:  c = d
␈↓ α,␈↓                f(a) = a
␈↓ α,␈↓                a = c
␈↓ α,␈↓        Derive: f(f(a)) = d

␈↓ α,␈↓Ex. 4:  Given:  f(b) = a
␈↓ α,␈↓                f(a) = a
␈↓ α,␈↓                f(f(a)) = c
␈↓ α,␈↓        Derive: f(f(b)) = c

␈↓ α,␈↓Ex. 5:  Given:  f(a,b) ␈↓↓≠␈↓ f(c,d)
␈↓ α,␈↓                a = c
␈↓ α,␈↓        Derive: b ␈↓↓≠␈↓ d

␈↓ α,␈↓Note␈α∪that␈α∀these␈α∪examples,␈α∪and␈α∀all␈α∪future␈α∪examples,␈α∀are␈α∪written␈α∪in␈α∀the␈α∪more␈α∀familiar␈α∪infix


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα1␈↓ ,



␈↓ α,␈↓functional␈α∂notation␈α∂although␈α∂our␈α∂algorithm␈α∂will␈α∞be␈α∂for␈α∂formulas␈α∂written␈α∂in␈α∂a␈α∂prefix␈α∞functional
␈↓ α,␈↓notation.

␈↓ α,␈↓The␈α
motivation␈α
behind␈α
this␈α
endeavor␈α
is␈α
to␈α
be␈α
able␈α
to␈α
prove␈α
syntactic␈α
equivalence␈α
between␈α
LISP[1]
␈↓ α,␈↓programs.␈α This␈αspecific␈αequality␈αproblem␈αis␈αsolved␈αby␈αresolution␈αtheorem␈αprovers[2]␈αsince␈αwe␈αfall
␈↓ α,␈↓into␈α∂the␈α∂domain␈α∂of␈α∂propositional␈α∂calculus␈α∂with␈α∂equality.␈α∂ However,␈α∂such␈α∂methods␈α⊂are␈α∂generally
␈↓ α,␈↓characterized␈α
by␈α
large␈αtime␈α
and␈α
space␈α
requirements␈αwhen␈α
the␈α
length␈α
of␈αtheorems␈α
or␈α
the␈αnumber␈α
of
␈↓ α,␈↓axioms␈α
increase.␈α
 In␈α
this␈α
report␈α
our␈α
attention␈α
is␈α
focused␈α
on␈α
equality␈α
from␈α
the␈α
standpoint␈α
of␈α
identity
␈↓ α,␈↓(i.e.␈αequality␈αby␈αvirtue␈αof␈αsubstitution␈αof␈αidentical␈αformulas).␈α In␈αa␈αsubsequent␈αreport␈αwe␈αshall␈αdeal
␈↓ α,␈↓with␈αequality␈αbased␈αon␈αthe␈αnotion␈αof␈αcopy␈α(i.e.␈αtwo␈αitems␈αare␈αequal␈αby␈αvirtue␈αof␈αtheir␈αbeing␈αcopies
␈↓ α,␈↓of␈αone␈αanother␈αor␈αeven␈αbeing␈αpartially␈αidentical␈αand␈αpartially␈αcopies␈αof␈αone␈αanother).␈α The␈αnotion
␈↓ α,␈↓of␈αcopy␈αas␈αexplained␈αhere␈α
has␈αno␈αrelevance␈αin␈αthe␈α
propositional␈αcalculus␈αsense;␈αhowever,␈αwhen␈α
the
␈↓ α,␈↓functions␈α⊂are␈α⊂viewed␈α⊃as␈α⊂returning␈α⊂values␈α⊃which␈α⊂are␈α⊂pointers␈α⊂to␈α⊃LISP␈α⊂list␈α⊂structures,␈α⊃then␈α⊂the
␈↓ α,␈↓notion␈αof␈α
copy␈αassumes␈α
its␈αimportance.␈α The␈α
ensuing␈αdiscussion␈α
does␈αnot␈α
make␈αknowledge␈αof␈α
LISP
␈↓ α,␈↓necessary.


































␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα2␈↓ ,



␈↓ α,␈↓II.  OTHER APPROACHES

␈↓ α,␈↓One␈α
way␈α
of␈α
keeping␈α
track␈α
of␈α
the␈α
equivalences␈αis␈α
by␈α
means␈α
of␈α
equivalence␈α
classes.␈α
 When␈α
a␈αnew
␈↓ α,␈↓equality␈α
is␈α
seen,␈α
the␈α
current␈αlist␈α
of␈α
equivalences␈α
is␈α
updated␈αto␈α
reflect␈α
all␈α
possible␈α
members␈αbased␈α
on
␈↓ α,␈↓the␈α⊂new␈α⊃equality.␈α⊂ One␈α⊂pitfall␈α⊃of␈α⊂such␈α⊃an␈α⊂approach␈α⊂is␈α⊃that␈α⊂all␈α⊂possible␈α⊃equalities␈α⊂can␈α⊃not␈α⊂be
␈↓ α,␈↓generated␈α
since␈α∞such␈α
a␈α∞procedure␈α
will␈α
not␈α∞terminate␈α
(e.g.␈α∞f(a)=a␈α
 will␈α
cause␈α∞substitution␈α
to␈α∞go␈α
on
␈↓ α,␈↓forever).␈α∞ A␈α
variation␈α∞of␈α∞this␈α
approach␈α∞is␈α
to␈α∞have␈α∞pointers␈α
to␈α∞all␈α
equivalence␈α∞classes.␈α∞ When␈α
an
␈↓ α,␈↓equality␈αis␈α
determined,␈αall␈α
subexpressions␈αof␈α
the␈αequality␈α
pair␈αthat␈α
appear␈αin␈αprevious␈α
equivalence
␈↓ α,␈↓classes␈α∞have␈α∂their␈α∞respective␈α∂pointers␈α∞substituted.␈α∂ Next,␈α∞the␈α∂class␈α∞name␈α∂of␈α∞the␈α∂new␈α∞equivalence
␈↓ α,␈↓class␈αis␈α
substituted␈αin␈α
all␈αequivalence␈αclasses␈α
where␈αmembers␈α
of␈αthe␈αnew␈α
equivalence␈αappear␈α
as␈αa
␈↓ α,␈↓subexpression.␈α Another␈αpitfall,␈αwhich␈αmust␈αbe␈αconsidered␈αin␈αall␈αapproaches,␈αis␈αthe␈αcase␈αwhen␈αtwo
␈↓ α,␈↓items␈α→are␈α→known␈α→to␈α→be␈α~inequivalent,␈α→yet␈α→subsequent␈α→equality␈α→operations␈α→could␈α~cause␈α→a
␈↓ α,␈↓contradiction.

␈↓ α,␈↓The␈αlast␈αpitfall␈αcan␈αbe␈αilustrated␈αby␈αexamining␈αa␈αvariant␈αof␈αexample␈α5.␈α In␈αthis␈αcase␈αwe␈αcould␈αnot
␈↓ α,␈↓assume,␈αin␈αaddition␈αto␈αthe␈αtwo␈αgiven␈αequalities,␈αthat␈αb=d␈αsince␈αthis␈αwould␈αlead␈αto␈αa␈αcontradiction.
␈↓ α,␈↓Namely,␈α
a=c␈αand␈α
b=d␈αimply␈α
that␈αf(a,b)=f(c,d)␈α
which␈αis␈α
known␈αto␈α
be␈αfalse.␈α
 Thus␈αthe␈α
fact␈αthat␈α
f(a,b)
␈↓ α,␈↓is␈α
known␈α
to␈α
be␈α
inequivalent␈α
to␈α
f(c,d)␈α
implies␈α
that␈α
a␈↓↓≠␈↓c␈α
or␈α
b␈↓↓≠␈↓d␈α
or␈α
both,␈α
but␈α
not␈α
equality␈α
(i.e.␈α
a=c␈α
and
␈↓ α,␈↓b=d).

␈↓ α,␈↓Closer␈αexamination␈αof␈αexample␈α4␈αwill␈αreveal␈αthat␈αin␈αeffect␈αf(f(b))␈αis␈αbeing␈αreduced␈αto␈αa␈αduring␈αthe
␈↓ α,␈↓process␈αof␈αtrying␈αto␈αprove␈αf(f(b))=c.␈α This␈αindicates␈αa␈αprocess␈αof␈αequivalence␈αby␈αreduction␈αwhich␈α
is
␈↓ α,␈↓like parsing.  Thus, our problem perhaps can be specified in terms of grammars.

␈↓ α,␈↓Given␈αa␈αgrammar␈αGS␈αfor␈αour␈αlanguage␈αof␈αformulas␈αwe␈αwish␈αto␈αdetermine␈αif␈αtwo␈αsentences␈αof␈αthe
␈↓ α,␈↓language␈αare␈α
equal␈αbased␈αon␈α
a␈αknown␈αset␈α
of␈αequalities.␈α
 The␈αset␈αof␈α
equalities␈αis␈αa␈α
set␈αof␈α
pairs␈αof
␈↓ α,␈↓strings␈α∂that␈α∞are␈α∂sentences␈α∞of␈α∂the␈α∞language␈α∂generated␈α∞by␈α∂GS␈α∞(henceforth␈α∂referred␈α∞to␈α∂as␈α∂L(GS)␈α∞).
␈↓ α,␈↓The␈αset␈αof␈αequalities␈αcan␈αbe␈αconsidered␈αto␈αbe␈αa␈αset␈αof␈αsymmetric␈αproductions␈αwhere␈αeach␈αmember
␈↓ α,␈↓of␈αthe␈αequality␈α
is␈αinterpreted␈αas␈αa␈α
nonterminal␈αsymbol␈αwith␈αan␈α
added␈αproduction␈αgoing␈α
from␈αthe
␈↓ α,␈↓nonterminal to its corresponding terminal symbol.

␈↓ α,␈↓For␈αexample,␈αFigure␈α
1␈αshows␈αhow␈αthe␈α
equality␈αf(a,b)=g(c)␈αwould␈αbe␈α
represented.␈α Note␈αthe␈α
use␈αof
␈↓ α,␈↓lower case letters for terminal symbols and upper case letters for nonterminal symbols.

␈↓ α,␈↓                        (f A B)  →→   (g C) 
␈↓ α,␈↓                         (g C)   →→  (f A B) 
␈↓ α,␈↓                           A     →→     a 
␈↓ α,␈↓                           B     →→     b 
␈↓ α,␈↓                           C     →→     c 

␈↓ α,␈↓                               Figure 1 


␈↓ α,␈↓Thus␈α∂the␈α∂problem␈α∂can␈α∂be␈α∂formulated␈α∂in␈α∂terms␈α∂of␈α∂formal␈α∂languages.␈α∂ Namely,␈α∂there␈α∂is␈α∂a␈α∂set␈α∞of
␈↓ α,␈↓productions,␈α∩GE,␈α∩containing␈α∩two␈α∩productions␈α∩for␈α⊃each␈α∩equality␈α∩and␈α∩one␈α∩production␈α∩for␈α⊃each
␈↓ α,␈↓terminal symbol.  The problem of equality determination can now be reformulated.



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα3␈↓ ,



␈↓ α,␈↓Given␈αa␈αpair␈αof␈αsentences␈αof␈αL(GS),␈αdetermine␈αif␈αafter␈αreducing␈αeach␈αterminal␈αsymbol␈αof␈αthe␈αfirst
␈↓ α,␈↓sentence,␈α∞say␈α
S1,␈α∞to␈α
its␈α∞corresponding␈α
nonterminal␈α∞symbol,␈α
the␈α∞set␈α
of␈α∞strings␈α
generated␈α∞from␈α
this
␈↓ α,␈↓string of nonterminals contains the second sentence, say S2.

␈↓ α,␈↓However,␈αGE␈αis␈α
a␈αtype␈α0␈α
grammar␈αwhose␈αdecision␈αproblem␈α
is␈αundecidable␈α(decidable␈α
for␈αcontext
␈↓ α,␈↓sensitive␈αgrammars␈α
but␈αGE␈α
is␈αnot␈αsuch␈α
a␈αgrammar␈α
since␈αfor␈αeach␈α
production␈αthe␈α
length␈αof␈αthe␈α
left
␈↓ α,␈↓hand␈αside␈α
of␈αthe␈αproduction␈α
is␈αnot␈αnecessarily␈α
less␈αthan␈αor␈α
equal␈αto␈αthe␈α
length␈αof␈αthe␈α
right␈αhand
␈↓ α,␈↓side␈α⊂of␈α⊂the␈α⊂production).␈α⊂ In␈α⊂other␈α⊂words␈α⊂the␈α⊂procedure␈α⊂of␈α⊂generating␈α⊂all␈α⊂sentences␈α⊂of␈α⊂a␈α⊂given
␈↓ α,␈↓length,␈α∩inefficient␈α∩as␈α∩it␈α∩might␈α∩be,␈α∩is␈α∩impossible.␈α∩ The␈α∩problem,␈α∩formulated␈α∩in␈α∩such␈α∪terms,␈α∩is
␈↓ α,␈↓undecidable␈α
for␈α
the␈α
general␈α
case.␈α
 One␈α
of␈α
the␈αbasic␈α
troubles␈α
of␈α
this␈α
approach␈α
is␈α
that␈α
it␈α
does␈αnot
␈↓ α,␈↓make␈α∞use␈α∞of␈α∞either␈α∞transitivity␈α∞information␈α∞or␈α∞the␈α∞syntax␈α∞of␈α∞L(GS).␈α∞ In␈α∞other␈α∞words␈α∞transitivity
␈↓ α,␈↓must␈αbe␈α
rederived␈αeach␈α
time␈αit␈α
is␈αdesired␈α
to␈αcheck␈α
if␈αtwo␈α
items␈αare␈α
equal.␈α An␈α
advantage␈αof␈αsuch␈α
a
␈↓ α,␈↓method,␈αif␈αit␈αwere␈αfeasible,␈αis␈αthat␈αwhen␈αnew␈αequality␈αrelations␈αare␈αdetermined,␈αupdating␈αthe␈αdata
␈↓ α,␈↓base consists of merely adding the symmetric productions.



































␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα4␈↓ ,



␈↓ α,␈↓III. SOLUTION

␈↓ α,␈↓The␈αprocedure␈αthat␈αwe␈αwill␈αuse␈αis␈αbased␈αon␈αsome␈αspecial␈αproperties␈αof␈αour␈αgrammar,␈αGS,␈αgiven␈αin
␈↓ α,␈↓Figure␈α2.␈α Note␈αthe␈αuse␈α
of␈α<atom>␈αto␈αindicate␈αa␈αvariable␈α
name.␈α Also␈αthere␈αis␈αone␈α
production␈αfor
␈↓ α,␈↓each␈α∞function␈α∂consisting␈α∞of␈α∂the␈α∞function␈α∞name,␈α∂and␈α∞as␈α∂many␈α∞S␈α∞symbols␈α∂as␈α∞there␈α∂are␈α∞arguments
␈↓ α,␈↓expected by the function.


␈↓ α,␈↓␈↓ ¬,S →→ <atom>
␈↓ α,␈↓␈↓ ¬,S →→ (<fname1> S S . . . S)
␈↓ α,␈↓␈↓ ¬,S →→ (<fname2> S S . . . S)
␈↓ α,␈↓␈↓ ¬,␈↓ ε,␈↓ εl.
␈↓ α,␈↓␈↓ ¬,␈↓ ε,␈↓ εl.
␈↓ α,␈↓␈↓ ¬,␈↓ ε,␈↓ εl.
␈↓ α,␈↓␈↓ ¬,S →→ (<fnameN> S S . . . S)

␈↓ α,␈↓␈↓ ¬,␈↓ ε,Figure 2



␈↓ α,␈↓The␈α
basic␈α
problem␈α
to␈α
which␈α
we␈α
will␈α
address␈α
ourselves␈α
is␈α
that␈α
of␈α
creating␈α
and␈α
updating␈α
a␈α
data␈α
base
␈↓ α,␈↓for␈α∞equalities␈α∞so␈α∂that␈α∞a␈α∞simple␈α∂decision␈α∞algorithm␈α∞can␈α∂be␈α∞used␈α∞to␈α∂determine␈α∞if␈α∞two␈α∂sentences␈α∞of
␈↓ α,␈↓L(GS)␈α⊃are␈α⊃indeed␈α⊃equal.␈α⊃ We␈α⊃will␈α⊃use␈α∩the␈α⊃notion␈α⊃of␈α⊃equivalence␈α⊃classes␈α⊃to␈α⊃keep␈α⊃track␈α∩of␈α⊃all
␈↓ α,␈↓sentences␈α
known␈αto␈α
be␈α
equal.␈α An␈α
equivalence␈α
class␈αis␈α
constructed␈α
for␈αeach␈α
valid␈α
sentence␈αof␈α
L(GS)
␈↓ α,␈↓which␈α
has␈α
been␈αencountered␈α
while␈α
processing␈αequalities␈α
of␈α
L(GS).␈α Moreover,␈α
the␈α
components␈αof
␈↓ α,␈↓each␈α⊂valid␈α∂sentence␈α⊂of␈α∂L(GS)␈α⊂are␈α∂represented␈α⊂in␈α∂terms␈α⊂of␈α∂their␈α⊂equivalence␈α∂classes.␈α⊂ This␈α⊂is␈α∂a
␈↓ α,␈↓crucial␈αproperty␈αof␈αthe␈αsystem␈αfor␈αit␈α
enables␈αthe␈αrepresentation␈αto␈αbe␈αrecursive␈α(i.e.␈αthe␈α
components
␈↓ α,␈↓of␈αan␈αequivalence␈αclass␈αmay␈αrefer␈αto␈αthe␈αclass).␈α In␈αfact␈αit␈αis␈αthis␈αproperty␈αwhich␈αdistinguishes␈αthe
␈↓ α,␈↓system␈α∂from␈α∂one␈α∂of␈α∂the␈α∂typical␈α∂approaches␈α∂mentioned␈α∂earlier␈α∂and␈α∂enables␈α∂us␈α∂to␈α∂represent␈α∂such
␈↓ α,␈↓equalities as f(a)=a .

␈↓ α,␈↓For␈α
example,␈α
if␈α
f(a)=f(b)␈α
,␈α
then␈α
when␈α
this␈α
equality␈α
is␈α
processed␈α
an␈α
equivalence␈α
class␈α
is␈α
created␈α
for␈α
a
␈↓ α,␈↓(say␈α∞A0),␈α∞for␈α∞f(a)␈α∞(say␈α
A1␈α∞whose␈α∞contents␈α∞is␈α∞f(A0)␈α
),␈α∞for␈α∞b␈α∞(say␈α∞A2),␈α
and␈α∞for␈α∞f(b)␈α∞(say␈α∞A3␈α
whose
␈↓ α,␈↓contents␈αis␈αf(A2)␈α).␈α The␈αequality␈αof␈αf(a)␈αand␈αf(b)␈αis␈αnoted␈αby␈αmerging␈αthe␈αtwo␈αequivalence␈αclasses
␈↓ α,␈↓A1␈α⊂and␈α⊂A3,␈α⊂and␈α⊃all␈α⊂subsequent␈α⊂references␈α⊂to␈α⊃f(a)␈α⊂or␈α⊂f(b)␈α⊂are␈α⊃by␈α⊂use␈α⊂of␈α⊂the␈α⊃lowest␈α⊂numbered
␈↓ α,␈↓equivalence␈αclass␈α
which␈αwas␈α
merged␈α-␈α
i.e␈α.␈α
A1␈αin␈α
our␈αcase.␈α
 As␈αanother␈α
example,␈αsuppose␈αa=b,␈α
then
␈↓ α,␈↓all␈αsubsequent␈αreferences␈αto␈αa␈αor␈αb␈αare␈αvia␈αtheir␈αclass␈αname␈α(i.e.␈αA0).␈α Thus␈αif␈αf(a)␈αor␈αf(b)␈αwere␈αto
␈↓ α,␈↓occur␈α⊂in␈α∂other␈α⊂sentences,␈α∂then␈α⊂they␈α⊂would␈α∂be␈α⊂represented␈α∂by␈α⊂a␈α∂unique␈α⊂equivalence␈α⊂class␈α∂name
␈↓ α,␈↓whose␈α⊂contents␈α⊃is␈α⊂f(A0).␈α⊂ A␈α⊃final␈α⊂example␈α⊂is␈α⊃ the␈α⊂representation␈α⊂of␈α⊃f(a)=a␈α⊂.␈α⊂ In␈α⊃this␈α⊂case␈α⊃a␈α⊂is
␈↓ α,␈↓identified␈αby␈αthe␈αequivalence␈α
class␈αA0,␈αwhile␈αf(a)␈αis␈α
identified␈αby␈αthe␈αequivalence␈αclass␈α
A1␈αwhose
␈↓ α,␈↓contents␈α
is␈αf(A0).␈α
 The␈αinstance␈α
of␈αequality␈α
is␈αrepresented␈α
by␈αthe␈α
fact␈αthat␈α
all␈αfuture␈α
references␈αto␈α
a
␈↓ α,␈↓and f(a) are by their equivalence class name -  i.e. A0.

␈↓ α,␈↓Thus␈αwe␈αsee␈αthat␈α
our␈αdata␈αbase␈αmust␈α
include␈αthe␈αvarious␈αequivalence␈α
classes␈αand␈αtheir␈αcontents␈α
in
␈↓ α,␈↓terms␈α∂of␈α∞other␈α∂equivalence␈α∞classes.␈α∂ At␈α∞this␈α∂point␈α∞it␈α∂becomes␈α∞clear␈α∂that␈α∞we␈α∂have␈α∂constructed␈α∞an
␈↓ α,␈↓equality␈α⊂grammar,␈α⊃GE,␈α⊂whose␈α⊂nonterminals␈α⊃are␈α⊂the␈α⊃names␈α⊂of␈α⊂the␈α⊃equivalence␈α⊂classes␈α⊃and␈α⊂the
␈↓ α,␈↓productions are simply the equivalence class names deriving each of their respective members.


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα5␈↓ ,



␈↓ α,␈↓The process of adding an equality to our data base consists of:

␈↓ α,␈↓1.␈α determine␈αfor␈αeach␈αhalf␈αof␈αthe␈αequality␈αthe␈αequivalence␈αclass␈αin␈αwhich␈αit␈αis␈αcontained␈α(and␈αthe
␈↓ α,␈↓creation of one if it is not contained in any equivalence class).

␈↓ α,␈↓2.  merge the two equivalence classes.

␈↓ α,␈↓3.  update all references to the merged equivalence classes to point to the new equivalence class.

␈↓ α,␈↓4.  merge all equivalence classes whose equivalence is a direct consequence of 2.

␈↓ α,␈↓As␈α∪a␈α∀clarification␈α∪of␈α∪4␈α∀consider␈α∪the␈α∀case␈α∪when␈α∪a=b,␈α∀and␈α∪f(a)␈α∪and␈α∀f(b)␈α∪appear␈α∀in␈α∪separate
␈↓ α,␈↓equivalence␈αclasses.␈α Then␈α2␈α implies␈αthat␈αf(a)␈αand␈αf(b)␈αare␈αuniquely␈αrepresented␈αas␈αf(ecln)␈α(ecln␈αis
␈↓ α,␈↓the␈α
name␈α∞of␈α
the␈α∞equivalence␈α
class␈α
containing␈α∞a=b),␈α
and␈α∞thus␈α
the␈α
two␈α∞classes␈α
containing␈α∞f(a)␈α
and
␈↓ α,␈↓f(b)␈α∩are␈α∩merged.␈α∩ In␈α∩other␈α∩words␈α∩all␈α∪classes␈α∩are␈α∩checked␈α∩against␈α∩each␈α∩other␈α∩for␈α∪elements␈α∩in
␈↓ α,␈↓common;␈α
and␈αif␈α
yes,␈α
then␈αa␈α
merge␈α
occurs␈αand␈α
only␈αone␈α
of␈α
the␈αduplicate␈α
entries␈α
is␈αkept␈α
in␈αthe␈α
newly
␈↓ α,␈↓formed equivalence class.

␈↓ α,␈↓The␈α
process␈α
of␈α
determining␈α
the␈α
equivalence␈α
class␈α∞containing␈α
a␈α
sentence␈α
of␈α
L(GS)␈α
is␈α
the␈α∞same␈α
as
␈↓ α,␈↓parsing␈αa␈αsentence␈αof␈αof␈αL(GS).␈α The␈αonly␈αdifference␈αis␈αthat␈αinstead␈αof␈αmaking␈αa␈αreduction␈αto␈αthe
␈↓ α,␈↓nonterminal␈α∞S␈α∞(and␈α
also␈α∞the␈α∞start␈α∞symbol),␈α
we␈α∞reduce␈α∞to␈α∞the␈α
appropriate␈α∞equivalence␈α∞class.␈α∞ If␈α
a
␈↓ α,␈↓reduction␈α
can␈αnot␈α
be␈αmade,␈α
then␈αthe␈α
sentence␈αis␈α
not␈αa␈α
member␈αof␈α
any␈αof␈α
the␈α
known␈αequivalence
␈↓ α,␈↓classes,␈α⊂and␈α⊂a␈α⊂new␈α⊂equivalence␈α⊂class␈α⊂(containing␈α⊂only␈α⊂the␈α⊂sentence␈α⊂in␈α⊂question)␈α⊂is␈α⊂created␈α⊂and
␈↓ α,␈↓parsing␈αcontinues.␈α Reductions,␈αif␈αthey␈αexist,␈αare␈αalways␈αunique␈αsince␈αany␈αsentence␈αis␈αcontained␈αin
␈↓ α,␈↓only␈α
one␈α∞equivalence␈α
class.␈α∞ In␈α
fact,␈α∞the␈α
ability␈α∞to␈α
add␈α∞equivalence␈α
classes␈α∞while␈α
parsing␈α∞is␈α
what
␈↓ α,␈↓enables us to prove that f(a)=f(b) given that a=b .

␈↓ α,␈↓Equality,␈α
in␈αgeneral,␈α
can␈αnot␈α
be␈α
determined␈αfor␈α
arbitrary␈αgrammars.␈α
 However,␈α
in␈αour␈α
case␈αGS␈α
has
␈↓ α,␈↓some␈αspecial␈αproperties.␈α The␈αmain␈αproblem␈αin␈αparsing␈αis␈αthat␈αthe␈αsentence␈αbeing␈αparsed␈αmay␈αnot
␈↓ α,␈↓be␈αin␈αany␈α
equivalence␈αclass.␈α This␈α
is␈αequivalent␈αto␈α
stating␈αthat␈αthere␈α
is␈αa␈αreduction␈α
to␈αbe␈αmade,␈α
yet
␈↓ α,␈↓there␈αis␈αno␈αnonterminal␈αsymbol␈αto␈αwhich␈αthe␈αhandle␈αis␈αto␈αbe␈αreduced.␈α In␈αour␈αcase␈αthe␈αproblem␈αis
␈↓ α,␈↓somewhat␈α∀alleviated␈α∪by␈α∀the␈α∀fact␈α∪that␈α∀GE␈α∀is␈α∪always␈α∀simple␈α∀precedence[3]␈α∪(see␈α∀proof␈α∀in␈α∪the
␈↓ α,␈↓appendix)␈α∂and␈α∂thus␈α∂we␈α∂always␈α∞know␈α∂when␈α∂a␈α∂reduction␈α∂is␈α∞desired.␈α∂ We␈α∂take␈α∂advantage␈α∂of␈α∞this
␈↓ α,␈↓situation␈αby␈αexamining␈αthe␈αequivalence␈αclasses␈αand␈αdetermining␈αif␈αa␈αreduction␈αexists.␈α If␈αyes,␈αthen
␈↓ α,␈↓the␈αreduction␈αis␈α
made␈αand␈αprocessing␈α
continues␈αin␈αa␈αnormal␈α
manner.␈α If␈αnot,␈α
then␈αit␈αis␈αknown␈α
that
␈↓ α,␈↓the␈αcurrent␈αhandle␈α(which␈αis␈αa␈αsentence␈αof␈αL(GS)␈α)␈αis␈αnot␈αa␈αmember␈αof␈αany␈αequivalence␈αclass,␈αand
␈↓ α,␈↓thus␈αa␈αnew␈αclass␈αis␈αcreated␈αwith␈αthe␈αhandle␈αas␈αits␈αsole␈αmember.␈α This␈αis␈αa␈αnatural␈αextension␈αto␈αthe
␈↓ α,␈↓process␈αof␈α
creating␈αa␈α
class␈αfor␈α
each␈αatom␈αnot␈α
already␈αin␈α
a␈αclass␈α
since␈αatoms␈α
are␈αalso␈αvalid␈α
sentences
␈↓ α,␈↓of␈α∀L(GS)␈α∀.␈α∃ By␈α∀atom␈α∀we␈α∀mean␈α∃variable␈α∀names␈α∀and␈α∀not␈α∃function␈α∀names.␈α∀ Note␈α∃that␈α∀since
␈↓ α,␈↓equivalence␈αclasses␈αalways␈α
contain␈αvalid␈αsentences␈α
of␈αL(GS),␈αthe␈α
equivalence␈αclasses␈αhave␈αthe␈α
same
␈↓ α,␈↓precedence␈αrelations␈αas␈αS␈α(the␈αstart␈αsymbol).␈α Also,␈αtwo␈αequivalence␈αclass␈αnames␈αcan␈αonly␈αhave␈αthe
␈↓ α,␈↓precedence␈α
relation␈α
=␈α
between␈α∞them,␈α
and␈α
in␈α
fact␈α
they␈α∞always␈α
have␈α
this␈α
relation.␈α∞ The␈α
remaining
␈↓ α,␈↓precedence␈α∞relations␈α∞are␈α∂given␈α∞in␈α∞the␈α∂precedence␈α∞matrix␈α∞in␈α∂Figure␈α∞3␈α∞(note␈α∂the␈α∞use␈α∞of␈α∂<ecln>␈α∞to
␈↓ α,␈↓denote an equivalence class name).

␈↓ α,␈↓In␈α∂the␈α∞ensuing␈α∂discussion␈α∞remember␈α∂that␈α∞we␈α∂are␈α∞always␈α∂dealing␈α∞with␈α∂valid␈α∞sentences␈α∂of␈α∞L(GS).
␈↓ α,␈↓The␈αreason␈αwe␈αcannot␈αhandle␈αarbitrary␈αgrammars␈αwith␈αour␈αalgorithm␈αis␈αthat␈αit␈αis␈αnot␈αusual␈αto␈αbe


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα6␈↓ ,



␈↓ α,␈↓able␈α
to␈α
identify␈αwhen␈α
a␈α
reduction␈α
is␈αto␈α
be␈α
made.␈α
 This␈αis␈α
true␈α
even␈α
if␈αwe␈α
have␈α
a␈αsimple␈α
precedence
␈↓ α,␈↓grammar␈α
since␈α
if␈α
a␈α
handle␈α
can␈αnot␈α
be␈α
identified,␈α
then␈α
it␈α
is␈αimpossible␈α
to␈α
tell␈α
when␈α
a␈α
reduction␈αis␈α
to
␈↓ α,␈↓be␈αmade.␈α This␈αrules␈αout␈αtop-down␈αparsing␈αmethods␈αsince␈αthey␈αoperate␈αby␈αfinding␈αreductions,␈αand
␈↓ α,␈↓if␈αsuch␈αreductions␈αdo␈αnot␈αexist,␈α
then␈αwe␈αcan't␈αvery␈αwell␈αknow␈α
when␈αthey␈αought␈αto␈αbe␈αcreated.␈α
 The
␈↓ α,␈↓primary␈α⊃reason␈α⊃for␈α⊃our␈α⊃success␈α⊃is␈α⊃that␈α⊃our␈α⊃grammar,␈α⊃GS,␈α⊃has␈α⊃only␈α⊃one␈α⊃non-terminal␈α⊂symbol,
␈↓ α,␈↓namely␈αthe␈αstart␈αsymbol.␈α Moreover,␈αall␈αequivalence␈αclasses␈αare␈αmerely␈αrenames␈αof␈αthe␈αstart␈α
symbol
␈↓ α,␈↓that␈α⊂allow␈α⊂us␈α∂to␈α⊂keep␈α⊂track␈α∂of␈α⊂what␈α⊂the␈α∂start␈α⊂symbol␈α⊂represents.␈α∂ Thus␈α⊂reductions␈α⊂are␈α⊂easy␈α∂to
␈↓ α,␈↓determine,␈αand,␈α
once␈αdetermined,␈αthe␈α
nonterminal␈αto␈αwhich␈α
the␈αhandle␈αis␈α
being␈αreduced␈α
is␈αeither
␈↓ α,␈↓found or created.

␈↓ α,␈↓The␈α
equality␈α∞data␈α
base␈α∞consists␈α
of␈α∞a␈α
set␈α∞of␈α
entries␈α
each␈α∞of␈α
which␈α∞is␈α
a␈α∞sentence␈α
of␈α∞L(GE).␈α
 Each
␈↓ α,␈↓entry␈α∞is␈α∂uniquely␈α∞numbered␈α∂and␈α∞has␈α∂a␈α∞left␈α∂part,␈α∞which␈α∂is␈α∞the␈α∂sentence␈α∞value,␈α∂and␈α∞a␈α∂right␈α∞part
␈↓ α,␈↓which␈α⊂is␈α⊃a␈α⊂pointer␈α⊃to␈α⊂the␈α⊂sentence␈α⊃representing␈α⊂the␈α⊃equivalence␈α⊂class␈α⊂to␈α⊃which␈α⊂it␈α⊃belongs.␈α⊂ A
␈↓ α,␈↓sentence␈αvalue␈α
is␈αeither␈α
an␈αatom␈α
or␈αa␈α
list␈αconsisting␈α
of␈αa␈α
function␈αname␈α
followed␈αby␈α
pointers␈αto␈α
the
␈↓ α,␈↓equivalence␈α∞classes␈α∞containing␈α∞the␈α∞arguments␈α∞of␈α∞the␈α∞function␈α∞being␈α∞represented␈α∞by␈α∞the␈α
sentence.
␈↓ α,␈↓Thus it is seen that each entry in the data base is a production:


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α3index →→ left 


␈↓ α,␈↓Also␈αnote␈αthat␈αall␈αreferences␈αto␈αa␈αmember␈αof␈αan␈αequivalence␈αclass␈αare␈αin␈αterms␈αof␈αits␈αhead␈α(i.e.␈αthe
␈↓ α,␈↓lowest␈α
numbered␈α
member␈α
of␈α
the␈α
equivalence␈α
class).␈α The␈α
nature␈α
of␈α
adding␈α
entries␈α
to␈α
the␈αdata␈α
base,
␈↓ α,␈↓and␈αthe␈αfact␈αthat␈αwhen␈αa␈αmerge␈αoccurs␈αthe␈αhead␈αof␈αthe␈αnew␈αequivalence␈αclass␈αbecomes␈αthe␈αlowest
␈↓ α,␈↓numbered␈αcomponent␈αof␈α
the␈αmerge␈αinsure␈αthat␈α
all␈αsentence␈αvalues␈αare␈α
in␈αterms␈αof␈αlower␈α
numbered
␈↓ α,␈↓equivalence␈αclasses.␈α Moreover,␈αby␈αstep␈α
5␈αof␈αthe␈αalgorithm␈αin␈α
Figure␈α4␈αno␈αsentence␈αis␈α
included␈αin
␈↓ α,␈↓more␈α∪than␈α∀one␈α∪equivalence␈α∪class,␈α∀and,␈α∪in␈α∪addition,␈α∀each␈α∪sentence␈α∪appears␈α∀only␈α∪once␈α∀in␈α∪an
␈↓ α,␈↓equivalence class.


␈↓ α,␈↓␈↓ ∧≤␈↓ ¬,<atom>␈↓ ε≤<fname>␈↓ π<<ecln>␈↓ λ\(␈↓ 	\)

␈↓ α,␈↓␈↓ ∧≤␈α?␈α?␈α∩<atom>␈↓ ¬,␈↓ ¬\>␈↓ ε≤␈↓ ε\␈↓ π<␈↓ π\>␈↓ λ\>␈↓ 	\>
␈↓ α,␈↓␈↓ ∧≤␈α?␈α?␈α
<fname>␈↓ ¬,␈↓ ¬\<␈↓ ε≤␈↓ ε\␈↓ π<␈↓ π\=␈↓ λ\<
␈↓ α,␈↓␈↓ ∧≤␈α?␈α?␈α→<ecln>␈↓ ¬,␈↓ ¬\<␈↓ ε≤␈↓ ε\␈↓ π<␈↓ π\=␈↓ λ\<␈↓ 	\=
␈↓ α,␈↓␈↓ ∧≤␈α?␈α?␈α=(␈↓ ¬,␈↓ ¬\␈↓ ε≤␈↓ ε\=
␈↓ α,␈↓␈↓ ∧≤␈α?␈α?␈α=)␈↓ ¬,␈↓ ¬\>␈↓ ε≤␈↓ ε\␈↓ π<␈↓ π\>␈↓ λ\>␈↓ 	\>

␈↓ α,␈↓␈↓ ∧≤␈↓ ¬,␈↓ ¬\␈↓ ε≤␈↓ ε\Figure 3










␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα7␈↓ ,



␈↓ α,␈↓␈↓ β,To add an equality pair:

␈↓ α,␈↓␈↓ β,1.  classl← result of parsing left half
␈↓ α,␈↓␈↓ β,2.  classr← result of parsing right half
␈↓ α,␈↓␈↓ β,3.  mods← nil
␈↓ α,␈↓␈↓ β,4.  a.  m← min(classl,classr)
␈↓ α,␈↓␈↓ β,    b.  n← max(classl,classr)
␈↓ α,␈↓␈↓ β,    c.  for j← m+1 step 1 until maxclass do begin
␈↓ α,␈↓␈↓ β,        if null(right(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else if atom(left(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else if member(m,cdr(left(eqtable[j]))) then mods← merge(j,mods)
␈↓ α,␈↓␈↓ β,        else nil
␈↓ α,␈↓␈↓ β,        end
␈↓ α,␈↓␈↓ β,    d.  for j← n step 1 until maxclass do begin
␈↓ α,␈↓␈↓ β,        if null(right(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else begin
␈↓ α,␈↓␈↓ β,            if right(eqtable[j]) = n then right(eqtable[j])← m ;
␈↓ α,␈↓␈↓ β,            subst(m,n,eql(eqtable[j]);
␈↓ α,␈↓␈↓ β,            if atom(left(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,            else if member(n,cdr(left(eqtable[j]))) then begin
␈↓ α,␈↓␈↓ β,                subst(m,n,cdr(left(eqtable[j]))) ;
␈↓ α,␈↓␈↓ β,                mods← merge(j,mods) ;
␈↓ α,␈↓␈↓ β,                end
␈↓ α,␈↓␈↓ β,            else nil ;
␈↓ α,␈↓␈↓ β,            end
␈↓ α,␈↓␈↓ β,5.  while not null(mods) do begin
␈↓ α,␈↓␈↓ β,        for k← 2 step 1 until length(mods) do begin
␈↓ α,␈↓␈↓ β,            if left(eqtable[mods[1]]) = left(eqtable[mods[k]]) then begin
␈↓ α,␈↓␈↓ β,                temp← right(eqtable[mods[k]]) ;
␈↓ α,␈↓␈↓ β,                mods← delete(k,mods) ;
␈↓ α,␈↓␈↓ β,                right(eqtable[mods[k]])← nil ;
␈↓ α,␈↓␈↓ β,                if right(eqtable[mods[1]]) ␈↓↓≠␈↓ temp then begin
␈↓ α,␈↓␈↓ β,                    classl← temp ;
␈↓ α,␈↓␈↓ β,                    classr← right(eqtable[mods[1]]) ;
␈↓ α,␈↓␈↓ β,                    go to 4 ;
␈↓ α,␈↓␈↓ β,                    end ;
␈↓ α,␈↓␈↓ β,                end ;
␈↓ α,␈↓␈↓ β,            end ;
␈↓ α,␈↓␈↓ β,        mods← cdr(mods) ;
␈↓ α,␈↓␈↓ β,        end

␈↓ α,␈↓␈↓ β,                                Figure 4







␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα8␈↓ ,



␈↓ α,␈↓IV.  EQUALITY DETERMINATION ALGORITHM

␈↓ α,␈↓In␈αthe␈αalgorithm,␈αgiven␈αin␈α
Figure␈α4,␈αeqtable␈αis␈αan␈αarray,␈α
accessed␈αby␈αleft␈αand␈αright,␈αwhich␈α
contains
␈↓ α,␈↓one␈αentry␈α
for␈αeach␈α
formula.␈α mods␈α
is␈αa␈αsorted␈α
list␈αin␈α
increasing␈αorder␈α
containing␈αpointers␈αto␈α
entries
␈↓ α,␈↓in␈α∞eqtable␈α∞which␈α∞refer␈α∞to␈α∞any␈α∂members␈α∞of␈α∞merged␈α∞equivalence␈α∞classes.␈α∞ maxclass␈α∞is␈α∂the␈α∞number
␈↓ α,␈↓associated␈α∞with␈α∞the␈α∞last␈α∂entry␈α∞in␈α∞eqtable.␈α∞ Note␈α∞that␈α∂the␈α∞algorithm's␈α∞implementation␈α∞is␈α∂far␈α∞more
␈↓ α,␈↓efficient␈α⊂than␈α⊂its␈α⊂representation␈α⊂here␈α⊂since␈α⊂we␈α⊂have␈α⊂put␈α⊂the␈α⊂emphasis␈α⊂on␈α⊂clarity.␈α⊂ For␈α⊂a␈α∂more
␈↓ α,␈↓efficient␈α∂representation␈α∂see␈α∂Figure␈α⊂5␈α∂and␈α∂also␈α∂the␈α∂discussion␈α⊂in␈α∂section␈α∂VII␈α∂on␈α∂time␈α⊂and␈α∂space
␈↓ α,␈↓requirements.

␈↓ α,␈↓The␈αalgorithm␈αterminates␈αsince␈αparsing␈α(steps␈α1-2)␈αis␈αa␈αprocess␈αthat␈αis␈αlimited␈αby␈αthe␈αlength␈αof␈αthe
␈↓ α,␈↓input␈αstring␈αand␈αby␈αthe␈αnumber␈αof␈αproductions.␈α Step␈α4␈αis␈αa␈αmerge␈αof␈αtwo␈αequivalence␈αclasses␈αand
␈↓ α,␈↓the␈α
time␈α
it␈α
takes␈αis␈α
bounded␈α
by␈α
the␈α
number␈αof␈α
productions.␈α
 Step␈α
5␈α
is␈αused␈α
to␈α
determine␈α
if␈αa␈α
merge
␈↓ α,␈↓of␈α
two␈α
equivalence␈α
classes␈α
is␈αto␈α
occur␈α
when␈α
a␈α
previous␈αmerge␈α
has␈α
caused␈α
two␈α
equivalence␈αclasses␈α
to
␈↓ α,␈↓have␈αan␈αelement␈αin␈αcommon.␈α If␈αthis␈αis␈αthe␈αcase,␈αthen␈αthe␈αtwo␈αequivalence␈αclasses␈αare␈αmerged␈αand
␈↓ α,␈↓the␈αresulting␈αclass␈αhas␈αonly␈αone␈αoccurrence␈αof␈αthe␈αpreviously␈αduplicate␈αentry.␈α In␈αorder␈αto␈αperform
␈↓ α,␈↓the␈αmerge␈α
the␈αalgorithm␈αis␈α
reapplied.␈α However,␈α
when␈αthe␈αalgorithm␈α
is␈αreapplied␈α
we␈αhave␈αone␈α
less
␈↓ α,␈↓equivalence␈α∞class␈α∞and␈α∞thus␈α∞by␈α∞the␈α∞well␈α∞ordering␈α∞principle␈α∞termination␈α∞is␈α∞guaranteed.␈α∞ If␈α∞no␈α∞two
␈↓ α,␈↓distinct␈α∪equivalence␈α∪classes␈α∪have␈α∪elements␈α∪in␈α∪common,␈α∪then␈α∪mods␈α∪is␈α∪exhausted␈α∪and␈α∀we␈α∪are
␈↓ α,␈↓through.␈α⊃ Note␈α⊂that␈α⊃if␈α⊂an␈α⊃equivalence␈α⊂class␈α⊃is␈α⊂found␈α⊃to␈α⊂contain␈α⊃a␈α⊂duplicate␈α⊃occurrence␈α⊃of␈α⊂an
␈↓ α,␈↓element␈α
after␈αa␈α
merge,␈α
then␈αthe␈α
duplicate␈αoccurrence␈α
is␈α
deleted␈αfrom␈α
the␈αclass.␈α
 This␈α
insures␈αthat
␈↓ α,␈↓our␈α
grammar␈α∞will␈α
always␈α∞have␈α
the␈α∞property␈α
that␈α∞no␈α
two␈α∞productions␈α
have␈α∞the␈α
same␈α∞right␈α
hand
␈↓ α,␈↓side.

␈↓ α,␈↓The␈αmotivation␈αbehind␈αstep␈α4␈αis␈αthe␈αpropogation␈αof␈αtransitivity␈αbetween␈αequivalence␈αclasses␈αwhile
␈↓ α,␈↓step␈α∀5␈α∃propogates␈α∀transitivity␈α∀via␈α∃function␈α∀application.␈α∀ In␈α∃other␈α∀words␈α∀functions␈α∃of␈α∀equal
␈↓ α,␈↓arguments␈α
are␈α
equal␈α
and␈α
thus␈α
their␈α
equivalence␈αclasses␈α
are␈α
merged.␈α
 Step␈α
4c␈α
and␈α
4d␈α
insert␈αin␈α
mods
␈↓ α,␈↓all␈α∞entries␈α∞that␈α∂are␈α∞affected␈α∞by␈α∂the␈α∞merge␈α∞of␈α∂equivalence␈α∞classes␈α∞-␈α∂i.e.␈α∞only␈α∞these␈α∂sentences␈α∞refer
␈↓ α,␈↓directly␈α∞to␈α∞the␈α∞two␈α∞items␈α
whose␈α∞equivalence␈α∞classes␈α∞have␈α∞been␈α
merged.␈α∞ Similarly,␈α∞step␈α∞5␈α∞is␈α
only
␈↓ α,␈↓applied␈α
to␈α
entries␈α
in␈α
mods␈α
because␈α
only␈α
these␈α
entries␈α
can␈α
possibly␈α
generate␈α
new␈α
equivalences.␈α
 This
␈↓ α,␈↓takes␈αadvantage␈αof␈α
the␈αfact␈αthat␈αprior␈α
to␈αthe␈αapplication␈αof␈α
the␈αalgorithm␈αthe␈α
equivalence␈αclasses
␈↓ α,␈↓are␈α∞disjoint,␈α∞and␈α∞thus␈α∞implied␈α∞equality␈α∞between␈α∞equivalence␈α∞classes␈α∞can␈α∞only␈α∞occur␈α∂via␈α∞elements
␈↓ α,␈↓pointing to the merged equivalence classes (this is an inductive argument).

␈↓ α,␈↓If␈α
mods␈α
is␈α∞not␈α
sorted␈α
then␈α∞step␈α
5␈α
would␈α∞not␈α
be␈α
as␈α
simple␈α∞since␈α
there␈α
would␈α∞be␈α
a␈α
question␈α∞as␈α
to
␈↓ α,␈↓which␈αof␈αmods(1)␈αor␈αmods(k)␈αshould␈αbe␈αdeleted.␈α The␈αreason␈αmods(k)␈αis␈αalways␈αdeleted␈αis␈αthat␈αthe
␈↓ α,␈↓equivalence␈αclass␈αto␈αwhich␈αit␈α
belongs␈αcan␈αnot␈αbe␈αboth␈α
greater␈αthan␈αmods(1)␈αand␈αthe␈α
minimum␈αof
␈↓ α,␈↓the␈αclasses␈αcontaining␈αmods(1)␈αand␈αmods(k).␈α Thus␈αeven␈αwhen␈αmods(k)␈αis␈αdeleted,␈αthe␈αproperty␈αof
␈↓ α,␈↓the data base having all entries point to lower numbered entries is preserved.

␈↓ α,␈↓Equality␈α⊃can␈α⊃be␈α⊃determined␈α⊃quite␈α⊃easily.␈α⊃ We␈α⊃simply␈α⊃parse␈α⊃the␈α⊃two␈α⊃items␈α⊃in␈α⊃question␈α∩in␈α⊃the
␈↓ α,␈↓following manner:

␈↓ α,␈↓1.␈α⊂ Parse␈α⊂one␈α⊂item␈α⊂with␈α⊂the␈α⊂existing␈α⊃set␈α⊂of␈α⊂productions␈α⊂modifying␈α⊂it␈α⊂whenever␈α⊂a␈α⊃reduction␈α⊂is
␈↓ α,␈↓encountered␈α∞which␈α∞has␈α∞no␈α∞corresponding␈α∞nonterminal␈α∞(i.e.␈α
the␈α∞sentence␈α∞is␈α∞not␈α∞a␈α∞member␈α∞of␈α
any
␈↓ α,␈↓equivalence class).



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈αα9␈↓ ,



␈↓ α,␈↓2.␈α∞ Parse␈α∞the␈α∞second␈α
item␈α∞with␈α∞the␈α∞modified␈α
grammar␈α∞from␈α∞part␈α∞1.␈α
 If␈α∞the␈α∞two␈α∞items␈α∞are␈α
equal,
␈↓ α,␈↓then␈αno␈αmodifications␈αto␈αthe␈α
grammar␈αwill␈αbe␈αnecessary␈αat␈α
this␈αstage.␈α In␈αfact,␈αif␈αany␈α
modifications
␈↓ α,␈↓were␈α∞made,␈α∞then␈α∞the␈α∞items␈α∂are␈α∞not␈α∞equal␈α∞(i.e.␈α∞it␈α∞is␈α∂impossible␈α∞to␈α∞determine␈α∞if␈α∞the␈α∞two␈α∂items␈α∞are
␈↓ α,␈↓equal based on equality information at hand).

␈↓ α,␈↓3.␈α
 If␈α
the␈α
resulting␈αequivalence␈α
class␈α
names␈α
from␈αthe␈α
parses␈α
are␈α
identical,␈αthen␈α
the␈α
two␈α
items␈αare
␈↓ α,␈↓equal.  Otherwise, they are not known to be equal.

␈↓ α,␈↓At this point we must prove that statement 3 is true.  This is equivalent to the following theorem:

␈↓ α,␈↓␈↓&Theorem:␈↓'β  The algorithm for determining equality is complete.

␈↓ α,␈↓␈↓&Proof:␈↓'β  The theorem is a direct consequence of the following two lemmas:

␈↓ α,␈↓␈↓&Lemma 1:␈↓'β  If the algorithm indicates that two items are equal, then they are equal.

␈↓ α,␈↓␈↓&Proof:␈↓'β␈α
 This␈α
statement␈α
is␈α
true␈α
since␈αby␈α
construction␈α
the␈α
equality␈α
updating␈α
algorithm␈α
insures␈αthat
␈↓ α,␈↓all elements in an equivalence class are equal.

␈↓ α,␈↓␈↓&Lemma 2:␈↓'β  If two items are equal, then the algorithm will so indicate.

␈↓ α,␈↓␈↓&Proof:␈↓'β␈α The␈αproof␈αof␈αthis␈αstatement␈αreduces␈αto␈αshowing␈αthat␈αif␈αtwo␈αitems␈αare␈αequal,␈αthen␈αthey␈αwill
␈↓ α,␈↓appear␈αin␈αthe␈αsame␈αequivalence␈αclass.␈α This␈αis␈αproved␈αby␈αconsidering␈αthe␈αtwo␈αways␈αin␈α
which␈αtwo
␈↓ α,␈↓items can be equal.

␈↓ α,␈↓a.␈α The␈αitems␈αwere␈αexplicitly␈αequal.␈α In␈αthis␈α
case␈αthey␈αwill␈αappear␈αin␈αthe␈αsame␈αequivalence␈αclass␈α
by
␈↓ α,␈↓virtue␈α∪of␈α∀step␈α∪4␈α∪of␈α∀the␈α∪updating␈α∀algorithm␈α∪and␈α∪hence␈α∀are␈α∪always␈α∪referred␈α∀to␈α∪by␈α∀the␈α∪new
␈↓ α,␈↓equivalence class name.

␈↓ α,␈↓b.␈α The␈αitems␈αbecame␈αequal␈αvia␈αtransitivity␈αand␈αor␈αfunctional␈αapplication.␈α In␈αthis␈αcase␈αthe␈αitems,
␈↓ α,␈↓say A and B, are equal to some third item C and now:

␈↓ α,␈↓Either␈α
 i.␈α
 C␈αmust␈α
be␈α
in␈αneither␈α
equivalence␈α
class␈α
which␈αis␈α
impossible␈α
by␈αstep␈α
5␈α
of␈α
the␈αupdating
␈↓ α,␈↓algorithm which examines all transitivities and function application of equals.

␈↓ α,␈↓Or␈α∞ ii.␈α∞ C␈α
must␈α∞be␈α∞an␈α
element␈α∞of␈α∞both␈α
equivalence␈α∞classes.␈α∞ This␈α
is␈α∞impossible␈α∞since␈α∞this␈α
means
␈↓ α,␈↓that␈α
there␈α
exist␈α
two␈α
leftmost␈α
derivations␈α
of␈α
C␈α
thereby␈α
contradicting␈α
the␈α
unambiguousness␈α
of␈αGE
␈↓ α,␈↓which␈α
is␈α
true␈α
by␈α
virtue␈α∞of␈α
GE␈α
being␈α
simple␈α
precedence.␈α∞ Therefore␈α
if␈α
two␈α
items␈α
are␈α∞equal,␈α
then
␈↓ α,␈↓they will be in the same equivalence class.

␈↓ α,␈↓Thus the above algorithm for determining equality is complete.

␈↓ α,␈↓A␈α∞more␈α∞efficient␈α∞implementation␈α∞of␈α∞the␈α∞equality␈α∞updating␈α∞algorithm␈α∞is␈α∞given␈α∞in␈α∞Figure␈α∞5.␈α∞ It␈α∞is
␈↓ α,␈↓different␈α∞from␈α∂the␈α∞algorithm␈α∂given␈α∞in␈α∞Figure␈α∂4␈α∞in␈α∂that␈α∞the␈α∞number␈α∂of␈α∞passes␈α∂over␈α∞the␈α∂table␈α∞is
␈↓ α,␈↓reduced.␈α In␈α
addition,␈αit␈αis␈α
made␈αmore␈αsuitable␈α
to␈αa␈αLISP-like␈α
implementation␈αwhere␈α
the␈αnumber
␈↓ α,␈↓of␈α
copy␈α
operations␈α
is␈α
to␈α
be␈α
minimized.␈α
 Note␈α
that␈α
mods␈α
is␈α
now␈α
a␈α
sorted␈α
list␈α
in␈α∞decreasing␈α
order,
␈↓ α,␈↓rather␈αthan␈αincreasing␈α
order,␈αcontaining␈αpointers␈αto␈α
entries␈αin␈αeqtable␈α
which␈αrefer␈αto␈αany␈α
members


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:10␈↓ ,



␈↓ α,␈↓of␈α∂merged␈α∞equivalence␈α∂classes.␈α∞ Also␈α∂we␈α∞have␈α∂added␈α∂a␈α∞parameter␈α∂dels␈α∞which␈α∂is␈α∞a␈α∂sorted␈α∂list␈α∞in
␈↓ α,␈↓decreasing␈αorder␈αcontaining␈α
the␈αnames␈αof␈α
eqtable␈αentries␈αwhich␈α
are␈αto␈αbe␈α
deleted.␈α The␈αpurpose␈α
of
␈↓ α,␈↓dels␈αis␈αshown␈αby␈αstep␈α7␈αwhich␈αremoves␈αfrom␈αeqtable␈αall␈αentries␈αthat␈αstep␈α8␈αhas␈αfound␈αnecessary␈αto
␈↓ α,␈↓delete.␈α Upon␈αexiting␈αstep␈α7,␈αdels␈αis␈αguaranteed␈αto␈αbe␈αempty␈αbecause␈αits␈αminimum␈αentry␈αis␈αgreater
␈↓ α,␈↓than␈αor␈αequal␈αto␈αn␈α(i.e.␈αmax(classl,classr))␈αsince␈αn␈αis␈αthe␈αhead␈αof␈αthe␈αclass␈αcontaining␈αthe␈αminimum
␈↓ α,␈↓entry␈α∩of␈α⊃dels.␈α∩ Step␈α⊃9␈α∩is␈α⊃used␈α∩to␈α⊃purge␈α∩the␈α⊃class␈α∩names␈α⊃in␈α∩dels␈α⊃from␈α∩eqtable␈α⊃when␈α∩mods␈α⊃is
␈↓ α,␈↓exhausted (i.e. we are through and thus we will not return to step 7).










































␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:11␈↓ ,



␈↓ α,␈↓␈↓ β,To add an equality pair:

␈↓ α,␈↓␈↓ β,1.  classl← result of parsing left half
␈↓ α,␈↓␈↓ β,2.  classr← result of parsing right half
␈↓ α,␈↓␈↓ β,3.  mods← nil
␈↓ α,␈↓␈↓ β,4.  dels← nil
␈↓ α,␈↓␈↓ β,5.  m← min(classl,classr)
␈↓ α,␈↓␈↓ β,6.  n← max(classl,classr)
␈↓ α,␈↓␈↓ β,7.  for j← maxclass step -1 until m+1 do begin
␈↓ α,␈↓␈↓ β,        if null(right(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else if j = dels[1] then begin
␈↓ α,␈↓␈↓ β,            right(eqtable[j])← nil ;
␈↓ α,␈↓␈↓ β,            dels← cdr(dels) ;
␈↓ α,␈↓␈↓ β,            end
␈↓ α,␈↓␈↓ β,        else begin
␈↓ α,␈↓␈↓ β,            if right(eqtable[j]) = n then right(eqtable[j])← m ;
␈↓ α,␈↓␈↓ β,            if atom(left(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,            else if member(n,cdr(left(eqtable[j]))) then begin
␈↓ α,␈↓␈↓ β,                subst(m,n,cdr(left(eqtable[j]))) ;
␈↓ α,␈↓␈↓ β,                mods← merge(j,mods) ;
␈↓ α,␈↓␈↓ β,                end
␈↓ α,␈↓␈↓ β,            else if member(m,cdr(left(eqtable[j]))) then mods← merge(j,mods)
␈↓ α,␈↓␈↓ β,            else nil ;
␈↓ α,␈↓␈↓ β,            end
␈↓ α,␈↓␈↓ β,        end
␈↓ α,␈↓␈↓ β,8.  while not null(mods) do begin
␈↓ α,␈↓␈↓ β,        len← length(mods) ;
␈↓ α,␈↓␈↓ β,        for k← 2 step 1 until len do
␈↓ α,␈↓␈↓ β,            if left(eqtable[mods[1]]) = left(eqtable[mods[k]]) then
␈↓ α,␈↓␈↓ β,                if right(eqtable[mods[1]]) ␈↓↓≠␈↓ right(eqtable[mods[k]]) then begin
␈↓ α,␈↓␈↓ β,                    classl← right(eqtable[mods[k]]) ;
␈↓ α,␈↓␈↓ β,                    classr← right(eqtable[mods[1]]) ;
␈↓ α,␈↓␈↓ β,                    dels← reverse(mods[1] cons dels) ;
␈↓ α,␈↓␈↓ β,                    mods← cdr(mods) ;
␈↓ α,␈↓␈↓ β,                    go to 5 ;
␈↓ α,␈↓␈↓ β,                    end
␈↓ α,␈↓␈↓ β,                else begin
␈↓ α,␈↓␈↓ β,                    k← len ;
␈↓ α,␈↓␈↓ β,                    dels← mods[1] cons dels ;
␈↓ α,␈↓␈↓ β,                    end
␈↓ α,␈↓␈↓ β,            else nil ;
␈↓ α,␈↓␈↓ β,        mods← cdr(mods) ;
␈↓ α,␈↓␈↓ β,        end
␈↓ α,␈↓␈↓ β,9.  purge(dels,eqtable)

␈↓ α,␈↓␈↓ β,                                Figure 5



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:12␈↓ ,



␈↓ α,␈↓V.  EXAMPLES

␈↓ α,␈↓The␈α⊃updating␈α⊃algorithm␈α⊂can␈α⊃be␈α⊃described␈α⊂as␈α⊃incorporating␈α⊃one␈α⊂of␈α⊃the␈α⊃approaches␈α⊂mentioned
␈↓ α,␈↓earlier␈α
as␈αa␈α
solution␈αto␈α
the␈αproblem.␈α
 Parsing␈αis␈α
the␈αsame␈α
as␈αthe␈α
process␈αof␈α
substituting␈αclass␈α
names
␈↓ α,␈↓for␈α⊂all␈α⊂subexpressions␈α⊂known␈α⊂to␈α⊂be␈α⊂members␈α⊃of␈α⊂equivalence␈α⊂classes␈α⊂while␈α⊂step␈α⊂5␈α⊂is␈α⊃similar␈α⊂to
␈↓ α,␈↓substituting the newly derived equality everywhere it appears as a subexpression.

␈↓ α,␈↓In␈α
the␈α
following␈α
examples,␈αeach␈α
numbered␈α
line␈α
represents␈α
the␈αresult␈α
of␈α
either␈α
parsing␈α
a␈αsentence␈α
or
␈↓ α,␈↓updating␈α
the␈α
data␈α
base␈αto␈α
include␈α
a␈α
new␈αequality.␈α
 In␈α
the␈α
former␈αcase␈α
only␈α
the␈α
modifications␈αto␈α
the
␈↓ α,␈↓data␈αbase,␈αeqtable,␈αare␈αshown␈αwhile␈αin␈αthe␈αlatter␈αcase␈αthe␈αentire␈αupdated␈αdata␈αbase␈αis␈αshown.␈α
 Also
␈↓ α,␈↓in␈α⊂the␈α⊂former␈α⊂case␈α⊂the␈α∂name␈α⊂of␈α⊂the␈α⊂equivalence␈α⊂class␈α∂containing␈α⊂the␈α⊂sentence␈α⊂being␈α⊂parsed␈α∂is
␈↓ α,␈↓returned.

␈↓ α,␈↓As␈αan␈αexample␈αof␈αthe␈αupdating␈αalgorithm,␈αwe␈αwill␈αshow␈αhow␈αthe␈αdata␈αbase␈αis␈αcreated␈αand␈αhow␈αan
␈↓ α,␈↓equality is determined for example 4.


␈↓ α,␈↓␈↓ β≤␈↓&sentence␈↓'β␈↓ ¬≤␈↓ εL␈↓ π<␈↓&eqtable␈↓'β␈↓ λ|␈↓ 	|␈↓&result␈↓'β

␈↓ α,␈↓␈↓ β≤1.  f(b)␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0␈↓ 	|returns A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< f(A0)␈↓ λ|A1

␈↓ α,␈↓␈↓ β≤2.  a␈↓ ¬≤yields␈↓ εLA2:␈↓ π< a␈↓ λ|A2␈↓ 	|returns A2

␈↓ α,␈↓␈↓ β≤3.  f(b)= a␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A1

␈↓ α,␈↓␈↓ β≤4.  f(a)␈↓ ¬≤yields␈↓ εLA3:␈↓ π< f(A1)␈↓ λ|A3␈↓ 	|returns A3

␈↓ α,␈↓␈↓ β≤5.  a␈↓ ¬≤yields␈↓ εL␈↓ π<no change␈↓ λ|␈↓ 	|returns A1

␈↓ α,␈↓␈↓ β≤6.  f(a) = a␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A1)␈↓ λ|A1

␈↓ α,␈↓␈↓ β≤7.  f(f(a))␈↓ ¬≤yields␈↓ εL␈↓ π<no change␈↓ λ|␈↓ 	|returns A1

␈↓ α,␈↓␈↓ β≤8.  c␈↓ ¬≤yields␈↓ εLA4:␈↓ π< c␈↓ λ|A4␈↓ 	|returns A4

␈↓ α,␈↓␈↓ β≤9.  c = f(f(a))␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A1)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA4:␈↓ π< c␈↓ λ|A1



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:13␈↓ ,



␈↓ α,␈↓At this point we wish to determine if f(f(b)) = c

␈↓ α,␈↓f(f(b)) gets parsed successively as:
␈↓ α,␈↓        1.  f(f(A0))
␈↓ α,␈↓        2.  f(A1)
␈↓ α,␈↓        3.  A1
␈↓ α,␈↓and c gets parsed as A1 and thus  f(f(b)) = c .

␈↓ α,␈↓As a more complicated example we now examine example 2.

␈↓ α,␈↓␈↓ β≤␈↓&sentence␈↓'β␈↓ ¬≤␈↓ εL␈↓ π<␈↓&eqtable␈↓'β␈↓ λ|␈↓ 	|␈↓&result␈↓'β

␈↓ α,␈↓␈↓ β≤1.  g(b)␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0␈↓ 	|returns A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1

␈↓ α,␈↓␈↓ β≤2.  f(a)␈↓ ¬≤yields␈↓ εLA2:␈↓ π< a␈↓ λ|A2␈↓ 	|returns A3
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A2)␈↓ λ|A3

␈↓ α,␈↓␈↓ β≤3.  g(b) = f(a)␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A2
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A2)␈↓ λ|A1

␈↓ α,␈↓␈↓ β≤4.  g(c)␈↓ ¬≤yields␈↓ εLA4:␈↓ π< c␈↓ λ|A4␈↓ 	|returns A5
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA5:␈↓ π< g(A4)␈↓ λ|A5

␈↓ α,␈↓␈↓ β≤5.  f(b)␈↓ ¬≤yields␈↓ εLA6:␈↓ π< f(A0)␈↓ λ|A6␈↓ 	|returns A6

␈↓ α,␈↓␈↓ β≤6.  g(c) = f(b)␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A2
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A2)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA4:␈↓ π< c␈↓ λ|A4
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA5:␈↓ π< g(A4)␈↓ λ|A5
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA6:␈↓ π< f(A0)␈↓ λ|A5

␈↓ α,␈↓␈↓ β≤7.  a␈↓ ¬≤yields␈↓ εL␈↓ π<no change␈↓ λ|␈↓ 	|returns A2

␈↓ α,␈↓␈↓ β≤8.  b␈↓ ¬≤yields␈↓ εL␈↓ π<no change␈↓ λ|␈↓ 	|returns A0

␈↓ α,␈↓␈↓ β≤9.  a = b␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA4:␈↓ π< c␈↓ λ|A4
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA5:␈↓ π< g(A4)␈↓ λ|A5
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA6:␈↓ π< f(A0)␈↓ λ|A5


␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:14␈↓ ,



␈↓ α,␈↓␈↓ β≤␈↓ ¬≤followed by␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA4:␈↓ π< c␈↓ λ|A4
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA5:␈↓ π< g(A4)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA6:␈↓ π< f(A0)␈↓ λ|NIL

␈↓ α,␈↓␈↓ β≤10. c␈↓ ¬≤yields␈↓ εL␈↓ π<no change␈↓ λ|␈↓ 	|returns A4

␈↓ α,␈↓␈↓ β≤11. d␈↓ ¬≤yields␈↓ εLA7:␈↓ π< d␈↓ λ|A7␈↓ 	|returns A7

␈↓ α,␈↓␈↓ β≤12. c = d␈↓ ¬≤yields␈↓ εLA0:␈↓ π< b␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA1:␈↓ π< g(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA2:␈↓ π< a␈↓ λ|A0
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA3:␈↓ π< f(A0)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA4:␈↓ π< c␈↓ λ|A4
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA5:␈↓ π< g(A4)␈↓ λ|A1
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA6:␈↓ π< f(A0)␈↓ λ|NIL
␈↓ α,␈↓␈↓ β≤␈↓ ¬≤␈↓ εLA7:␈↓ π< d␈↓ λ|A4


␈↓ α,␈↓At this point we wish to determine if g(a) = g(d)

␈↓ α,␈↓g(a) gets parsed successively as:
␈↓ α,␈↓        1.  g(A0)
␈↓ α,␈↓        2.  A1
␈↓ α,␈↓and g(d) gets parsed successively as:
␈↓ α,␈↓        1.  g(A4)
␈↓ α,␈↓        2.  A1
␈↓ α,␈↓and thus g(a) = g(d) .


















␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:15␈↓ ,



␈↓ α,␈↓VI.  INEQUALITY DETERMINATION

␈↓ α,␈↓Until␈α⊂now␈α⊂we␈α⊂have␈α∂shown␈α⊂how␈α⊂the␈α⊂question␈α∂of␈α⊂whether␈α⊂two␈α⊂items␈α∂are␈α⊂known␈α⊂to␈α⊂be␈α⊂equal␈α∂is
␈↓ α,␈↓answered.␈α∞ However,␈α∞the␈α∞question␈α∞of␈α∞equality␈α
has␈α∞two␈α∞additional␈α∞possible␈α∞answers.␈α∞ Namely,␈α
the
␈↓ α,␈↓items␈α∂may␈α∂be␈α⊂unequal␈α∂or␈α∂no␈α∂information␈α⊂as␈α∂to␈α∂their␈α∂equality␈α⊂is␈α∂known.␈α∂ Determination␈α⊂of␈α∂the
␈↓ α,␈↓answer␈αto␈αthese␈αtwo␈αquestions␈αis␈αmore␈αcomplicated.␈α In␈αorder␈αto␈αfacilitate␈αsuch␈αwork␈αwe␈α
also␈αkeep
␈↓ α,␈↓track␈α∩of␈α∩equivalence␈α∪classes␈α∩which␈α∩are␈α∪known␈α∩to␈α∩be␈α∪unequal.␈α∩ This␈α∩is␈α∪done␈α∩via␈α∩a␈α∪table␈α∩of
␈↓ α,␈↓equivalence␈α
classes,␈α
ineqtable,␈α
which␈α
are␈α
known␈α
to␈α
be␈α
unequal.␈α
 This␈α
table␈α
is␈α
again␈α
accessed␈α
by␈α
left
␈↓ α,␈↓and␈αright.␈α Therefore,␈αwhenever␈αa␈αmerge␈αof␈α
two␈αequivalence␈αclasses␈αoccurs,␈αthis␈αtable␈αmust␈αalso␈α
be
␈↓ α,␈↓updated.␈α∞ This␈α
means␈α∞that␈α∞between␈α
steps␈α∞4b␈α∞and␈α
4c␈α∞of␈α∞the␈α
equality␈α∞determination␈α∞algorithm␈α
an
␈↓ α,␈↓update is made of the inequivalent classes.

␈↓ α,␈↓Two␈α
items␈α
may␈α
be␈α
shown␈αto␈α
be␈α
unequal␈α
explicitly␈α
or␈αimplicitly␈α
wheras␈α
two␈α
items␈α
are␈α
equal␈αonly
␈↓ α,␈↓explicitly.␈α The␈αprocess␈αof␈αparsing␈αallows␈αthe␈αbypassing␈αof␈αspecial␈αhandling␈αfor␈αimplied␈αequalities
␈↓ α,␈↓since␈αif␈αa␈αsentence␈αis␈αnot␈αin␈αthe␈αdata␈αbase,␈αthen␈αit␈αis␈αadded␈αto␈αit␈αwhile␈αbeing␈αparsed.␈α This␈αis␈αwhat
␈↓ α,␈↓enables␈α∞the␈α∞recognition␈α∞of␈α∞f(a)␈α∞=␈α
f(b)␈α∞ given␈α∞a␈α∞=␈α∞b␈α∞.␈α
 Implied␈α∞inequalities␈α∞are␈α∞also␈α∞quite␈α∞easy␈α
to
␈↓ α,␈↓detect.␈α∂ In␈α∂this␈α⊂case␈α∂two␈α∂sentences␈α∂are␈α⊂not␈α∂explicitly␈α∂known␈α∂to␈α⊂be␈α∂unequal␈α∂(i.e.␈α⊂the␈α∂equivalence
␈↓ α,␈↓classes␈α∂containing␈α∂them␈α∞are␈α∂not␈α∂known␈α∞to␈α∂be␈α∂unequal);␈α∞however,␈α∂when␈α∂they␈α∞are␈α∂assumed␈α∂to␈α∞be
␈↓ α,␈↓equal,␈αand␈αthereby␈αadded␈αto␈αthe␈αdata␈αbase,␈αthen␈αa␈αcontradiction␈αwill␈αoccur.␈α This␈αcontradiction␈αis
␈↓ α,␈↓manifested␈α∩at␈α⊃the␈α∩occurrence␈α⊃of␈α∩a␈α⊃merge␈α∩of␈α⊃two␈α∩equivalence␈α⊃classes␈α∩which␈α⊃are␈α∩known␈α∩to␈α⊃be
␈↓ α,␈↓unequal.␈α∀ Thus␈α∀it␈α∀is␈α∪seen␈α∀that␈α∀the␈α∀only␈α∪modification␈α∀needed␈α∀to␈α∀the␈α∀equality␈α∪determination
␈↓ α,␈↓algorithm␈αis␈αto␈αcheck␈αif␈αthe␈αtwo␈αabout␈αto␈αbe␈αmerged␈αequivalence␈αclasses␈αare␈αknown␈αto␈αbe␈αunequal.
␈↓ α,␈↓Moreover,␈α
if␈α
at␈α∞any␈α
time␈α
during␈α∞the␈α
implicit␈α
inequality␈α∞phase␈α
any␈α
entries␈α∞must␈α
be␈α
added␈α∞to␈α
the
␈↓ α,␈↓data base, then the sentences in question can not be implicitly equal.

␈↓ α,␈↓The␈α∞revised␈α
algorithm␈α∞for␈α
the␈α∞addition␈α
of␈α∞any␈α
equality␈α∞to␈α
the␈α∞data␈α
base␈α∞as␈α
well␈α∞as␈α
determining
␈↓ α,␈↓implicit␈α∂inequalities␈α∂is␈α∂given␈α∂in␈α∂Figure␈α∂6.␈α⊂ Note␈α∂the␈α∂use␈α∂of␈α∂maxneq␈α∂to␈α∂indicate␈α∂the␈α⊂number␈α∂of
␈↓ α,␈↓entries␈α∂in␈α⊂ineqtable.␈α∂ The␈α⊂proof␈α∂of␈α∂the␈α⊂completeness␈α∂of␈α⊂the␈α∂inequality␈α⊂determination␈α∂algorithm
␈↓ α,␈↓remains␈αthe␈αsame␈α
while␈αthe␈αproof␈αof␈α
the␈αcompleteness␈αof␈α
the␈αinequality␈αdetermination␈αalgorithm␈α
is
␈↓ α,␈↓similar␈α
to␈α
the␈α
former,␈α
and␈α
thus␈α
it␈α
will␈αnot␈α
be␈α
repeated.␈α
 Similarly,␈α
the␈α
algorithm␈α
can␈α
be␈αencoded
␈↓ α,␈↓more␈α∞efficiently␈α∞in␈α∂the␈α∞style␈α∞of␈α∞Figure␈α∂5␈α∞or␈α∞even␈α∂as␈α∞discussed␈α∞in␈α∞the␈α∂section␈α∞on␈α∞time␈α∂and␈α∞space
␈↓ α,␈↓requirements.

















␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:16␈↓ ,



␈↓ α,␈↓␈↓ β,To add an equality pair:

␈↓ α,␈↓␈↓ β,1.  classl← result of parsing left half
␈↓ α,␈↓␈↓ β,2.  classr← result of parsing right half
␈↓ α,␈↓␈↓ β,3.  mods← nil
␈↓ α,␈↓␈↓ β,4.  a.  m← min(classl,classr)
␈↓ α,␈↓␈↓ β,    b.  n← max(classl,classr)
␈↓ α,␈↓␈↓ β,    c.  for j← 1 step 1 until maxneq do begin
␈↓ α,␈↓␈↓ β,        if right(ineqtable[j]) = n then right(ineqtable[j])← m
␈↓ α,␈↓␈↓ β,        else if left(ineqtable[j]) = n then left(ineqtable[j])← m ;
␈↓ α,␈↓␈↓ β,        if left(ineqtable[j]) = right(ineqtable[j]) then "contradiction"
␈↓ α,␈↓␈↓ β,        else nil ;
␈↓ α,␈↓␈↓ β,        end
␈↓ α,␈↓␈↓ β,    d.  for j← m+1 step 1 until maxclass do begin
␈↓ α,␈↓␈↓ β,        if null(right(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else if atom(left(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else if member(m,cdr(left(eqtable[j]))) then mods← merge(j,mods)
␈↓ α,␈↓␈↓ β,        else nil
␈↓ α,␈↓␈↓ β,        end
␈↓ α,␈↓␈↓ β,    e.  for j← n step 1 until maxclass do begin
␈↓ α,␈↓␈↓ β,        if null(right(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,        else begin
␈↓ α,␈↓␈↓ β,            if right(eqtable[j]) = n then right(eqtable[j])← m ;
␈↓ α,␈↓␈↓ β,            subst(m,n,eql(eqtable[j]);
␈↓ α,␈↓␈↓ β,            if atom(left(eqtable[j])) then nil
␈↓ α,␈↓␈↓ β,            else if member(n,cdr(left(eqtable[j]))) then begin
␈↓ α,␈↓␈↓ β,                subst(m,n,cdr(left(eqtable[j]))) ;
␈↓ α,␈↓␈↓ β,                mods← merge(j,mods) ;
␈↓ α,␈↓␈↓ β,                end
␈↓ α,␈↓␈↓ β,            else nil ;
␈↓ α,␈↓␈↓ β,            end
␈↓ α,␈↓␈↓ β,2.  while not null(mods) do begin
␈↓ α,␈↓␈↓ β,        for k← 2 step 1 until length(mods) do begin
␈↓ α,␈↓␈↓ β,            if left(eqtable[mods[1]]) = left(eqtable[mods[k]]) then begin
␈↓ α,␈↓␈↓ β,                temp← right(eqtable[mods[k]]) ;
␈↓ α,␈↓␈↓ β,                mods← delete(k,mods) ;
␈↓ α,␈↓␈↓ β,                right(eqtable[mods[k]])← nil ;
␈↓ α,␈↓␈↓ β,                if right(eqtable[mods[1]]) ␈↓↓≠␈↓ temp then begin
␈↓ α,␈↓␈↓ β,                    classl← temp ;
␈↓ α,␈↓␈↓ β,                    classr← right(eqtable[mods[1]]) ;
␈↓ α,␈↓␈↓ β,                    go to 4 ;
␈↓ α,␈↓␈↓ β,                    end ;
␈↓ α,␈↓␈↓ β,                end ;
␈↓ α,␈↓␈↓ β,            end ;
␈↓ α,␈↓␈↓ β,        mods← cdr(mods) ;
␈↓ α,␈↓␈↓ β,        end

␈↓ α,␈↓␈↓ β,                                Figure 6

␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:17␈↓ ,



␈↓ α,␈↓VII.  TIME AND STORAGE REQUIREMENTS

␈↓ α,␈↓From␈α
a␈αcomputational␈α
complexity␈αstandpoint,␈α
the␈αequality␈α
determination␈αalgorithm␈α
is␈αquite␈α
simple.
␈↓ α,␈↓Specifically,␈α
in␈α
parsing␈α∞a␈α
sentence␈α
there␈α
are␈α∞exactly␈α
as␈α
many␈α
reductions␈α∞to␈α
be␈α
made␈α
as␈α∞there␈α
are
␈↓ α,␈↓atoms␈α
and␈α
function␈α∞names␈α
in␈α
the␈α∞sentence.␈α
 Moreover,␈α
the␈α∞constant␈α
of␈α
proportionality␈α∞is␈α
directly
␈↓ α,␈↓related␈αto␈α
the␈αsize␈α
of␈αthe␈α
data␈αbase␈α
since␈αthe␈α
latter␈αmust␈α
be␈αsearched␈α
for␈αthe␈αappropriate␈α
reduction.
␈↓ α,␈↓Of course, the search can be speeded up by keeping the data base sorted via a hashing function.

␈↓ α,␈↓A␈α∂more␈α∂careful␈α∞analysis␈α∂allows␈α∂us␈α∂to␈α∞determine␈α∂upper␈α∂bounds␈α∂on␈α∞the␈α∂storage␈α∂necessary␈α∂for␈α∞the
␈↓ α,␈↓equality␈αdata␈αbase␈αas␈α
well␈αas␈αdetermining␈αaverage␈α
times␈αfor␈αequality␈αdetermination␈α
and␈αupdating
␈↓ α,␈↓the␈αequality␈αdata␈αbase.␈α Specifically,␈αthe␈α
maximum␈αnumber␈αof␈αequivalence␈αclasses␈αpossible␈αis␈α
when
␈↓ α,␈↓all␈α∩the␈α⊃axioms␈α∩use␈α∩different␈α⊃functions␈α∩and␈α∩atoms.␈α⊃ In␈α∩this␈α⊃case␈α∩we␈α∩would␈α⊃need␈α∩at␈α∩most␈α⊃one
␈↓ α,␈↓equivalence␈α
class␈α
per␈αfunction␈α
and␈α
atom.␈α
 Thus␈αthe␈α
upper␈α
bound␈αon␈α
the␈α
number␈α
of␈αequivalence
␈↓ α,␈↓classes␈αis␈αthe␈αtotal␈αlength␈αof␈αthe␈αaxioms␈αin␈αthe␈αdata␈αbase␈α(say␈αn).␈α Each␈αequivalence␈αclass␈αrequires
␈↓ α,␈↓one␈α
pointer␈αto␈α
the␈α
head␈αof␈α
its␈α
class␈α(the␈α
right␈αfield␈α
of␈α
eqtable).␈α The␈α
left␈α
field␈αof␈α
each␈αeqtable␈α
entry
␈↓ α,␈↓requires␈αone␈α
location␈αfor␈αthe␈α
function␈αname␈αand␈α
one␈αpointer␈αfor␈α
each␈αargument.␈α
 The␈αmaximum
␈↓ α,␈↓number␈αof␈αpointers␈αand␈αlocations␈α
necessary␈αfor␈αthe␈αleft␈αfield␈αof␈α
all␈αentries␈αin␈αeqtable␈αis␈α2n-1.␈α
 This
␈↓ α,␈↓quantity␈α⊃is␈α∩achieved␈α⊃when␈α∩all␈α⊃atomic␈α∩arguments␈α⊃are␈α⊃unique␈α∩and␈α⊃thus␈α∩there␈α⊃are␈α∩no␈α⊃common
␈↓ α,␈↓subexpressions␈αas␈αwell␈αas␈αno␈αequality␈αrelations.␈α In␈αother␈αwords␈αthis␈αis␈αthe␈αworst␈αcase␈αfor␈α
a␈αsingle
␈↓ α,␈↓formula␈αcomprised␈αof␈αother␈αformulas␈αmeeting␈αthese␈αconditions.␈α The␈αtruth␈αof␈αthis␈αclaim␈αis␈αseen␈αby
␈↓ α,␈↓noting␈αthat␈αevery␈α
atom␈αrequires␈αtwo␈αleft␈α
field␈αentries␈α-␈α
one␈αfor␈αits␈αequivalence␈α
class␈αand␈αone␈αfor␈α
its
␈↓ α,␈↓occurrence␈α∞as␈α∞an␈α∞argument␈α∞in␈α∞another␈α∞formula,␈α∞and␈α∞every␈α∞instance␈α∞of␈α∞a␈α∞function␈α∞name␈α∂but␈α∞the
␈↓ α,␈↓outermost␈αone␈αrequires␈αtwo␈αleft␈αfield␈αentries␈α-␈α
one␈αfor␈αits␈αoccurrence␈αin␈αa␈αformula␈αand␈αone␈α
for␈αits
␈↓ α,␈↓formulas␈αoccurrence␈αas␈αan␈αargument␈αin␈αanother␈αformula.␈α Finally,␈αsince␈αformulas␈αare␈αnot␈αof␈αfixed
␈↓ α,␈↓length␈α
(i.e.␈α
they␈α
have␈α
a␈α
varying␈α
number␈α
of␈α
arguments),␈α
we␈α
need␈α
one␈α
marker␈α
pointer␈α
per␈α
eqtable
␈↓ α,␈↓entry␈α∂to␈α∂denote␈α⊂the␈α∂length␈α∂of␈α⊂its␈α∂left␈α∂field␈α⊂(or␈α∂depending␈α∂on␈α⊂the␈α∂method␈α∂of␈α⊂implementation␈α∂to
␈↓ α,␈↓denote␈αthe␈αfact␈αthat␈αthere␈αare␈αno␈αmore␈αarguments).␈α In␈αfact␈αwe␈αneed␈αone␈αsuch␈αpointer␈αper␈αeqtable
␈↓ α,␈↓entry␈αor␈αn␈αsuch␈αpointers␈αin␈αtotal.␈α Thus␈αat␈αthis␈αpoint␈αour␈αequality␈αdata␈αstructure␈αrequires␈αat␈αmost
␈↓ α,␈↓4n-1␈α∞pointers␈α∂in␈α∞order␈α∂to␈α∞be␈α∞able␈α∂to␈α∞handle␈α∂a␈α∞set␈α∂of␈α∞axioms␈α∞containing␈α∂a␈α∞sum␈α∂of␈α∞n␈α∂atoms␈α∞and
␈↓ α,␈↓function␈α
names.␈α
 Actually,␈α
this␈α
upper␈α
bound␈α
is␈α
4n-2m␈α
where␈α
m␈α
is␈α
the␈α
 ner␈α
of␈α
axioms␈αpresent.␈α
 Note
␈↓ α,␈↓the indistinguishability of pointers and locations.

␈↓ α,␈↓Both␈α⊂the␈α∂equality␈α⊂determination␈α∂and␈α⊂equality␈α∂data␈α⊂base␈α∂updating␈α⊂algorithms␈α∂need␈α⊂to␈α⊂do␈α∂table
␈↓ α,␈↓lookup␈α∀type␈α∀operations.␈α∀ This␈α∀is␈α∀a␈α∀factor␈α∀which␈α∀slows␈α∀down␈α∀these␈α∀algorithms␈α∀considerably.
␈↓ α,␈↓However,␈α∀the␈α∪problem␈α∀can␈α∪be␈α∀alleviated␈α∪by␈α∀use␈α∪of␈α∀hashing␈α∪for␈α∀the␈α∀equality␈α∪determination
␈↓ α,␈↓algorithm,␈α∂and␈α∂by␈α∂use␈α∂of␈α∞linked␈α∂lists␈α∂for␈α∂the␈α∂equality␈α∞data␈α∂base␈α∂updating␈α∂algorithm.␈α∂ For␈α∞each
␈↓ α,␈↓equivalence␈αclass␈αwe␈αwill␈αkeep␈α
a␈αlinked␈αlist␈αthrough␈αall␈αthe␈α
eqtable␈αentries␈αin␈αwhose␈αleft␈α
field␈αthe
␈↓ α,␈↓equivalence␈αclass␈α
appears.␈α Also␈α
a␈αlinked␈α
list␈αis␈αkept␈α
with␈αeach␈α
equivalence␈αclass␈α
for␈αall␈αthe␈α
eqtable
␈↓ α,␈↓entries␈αwhich␈αare␈αin␈αthe␈αequivalence␈αclass␈α(i.e.␈αidentical␈αright␈αfield␈αentries).␈α This␈αwill␈αadd␈αat␈αmost
␈↓ α,␈↓n␈αpointers␈αfor␈αhashing,␈αn␈αpointers␈αfor␈αthe␈αleft␈αfield␈αlinks,␈αn␈αpointers␈αfor␈αthe␈αheads␈αof␈αthe␈αleft␈αfield
␈↓ α,␈↓links,␈αand␈α
n␈αpointers␈α
for␈αthe␈α
heads␈αof␈α
the␈αright␈α
field␈αlinks.␈α
 Thus␈αthe␈α
new␈αmaximum␈α
number␈αof
␈↓ α,␈↓pointers␈α∂is␈α⊂8n-2m.␈α∂ However,␈α⊂it␈α∂will␈α⊂generally␈α∂be␈α∂the␈α⊂case␈α∂that␈α⊂two␈α∂pointers␈α⊂can␈α∂be␈α⊂stored␈α∂per
␈↓ α,␈↓computer␈αword␈αand␈αthus␈αthe␈αstorage␈αrequirement␈αis␈α4n-m␈αwords.␈α Actually,␈αwe␈αneed␈αslightly␈αmore
␈↓ α,␈↓storage␈α∪since␈α∩we␈α∪must␈α∪also␈α∩account␈α∪for␈α∪the␈α∩hash␈α∪ buckets.␈α∪ However,␈α∩this␈α∪amount␈α∪is␈α∩rather
␈↓ α,␈↓insignificant␈αin␈αlight␈αof␈αthe␈αrest␈αof␈αthe␈αrequired␈αstorage,␈αand␈αthus␈αwe␈αcan␈αincrease␈αthe␈αnumber␈αof
␈↓ α,␈↓buckets to reduce the probability of collisions in the table.



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:18␈↓ ,



␈↓ α,␈↓In␈α
order␈αto␈α
get␈αa␈α
better␈α
feeling␈αfor␈α
the␈αproposed␈α
data␈αstructure␈α
we␈α
give␈αa␈α
sample␈αentry␈α
in␈αFigure␈α
7.
␈↓ α,␈↓Note␈αthat␈αall␈αpointers␈αalways␈αrefer␈αto␈αthe␈αfirst␈αword␈αof␈αthe␈αentry.␈α This␈αdata␈αstructure␈αwill␈αreduce
␈↓ α,␈↓greatly␈αthe␈αamount␈αof␈αwork␈αthe␈αupdating␈αalgorithm␈αmust␈αdo␈αbecause␈αeach␈αof␈αthe␈αlinks␈αenables␈αthe
␈↓ α,␈↓quick␈α⊃execution␈α⊃of␈α∩one␈α⊃of␈α⊃the␈α∩steps.␈α⊃ The␈α⊃links␈α⊃between␈α∩eqtable␈α⊃entries␈α⊃containing␈α∩a␈α⊃certain
␈↓ α,␈↓equivalence␈α∃class␈α∃name␈α∃as␈α∃an␈α∃argument␈α∃and␈α∃the␈α∃links␈α∃connecting␈α∃all␈α∃entries␈α∃in␈α∃the␈α∀same
␈↓ α,␈↓equivalence␈α∪class␈α∩enable␈α∪the␈α∩quick␈α∪execution␈α∩of␈α∪steps␈α∩4d␈α∪and␈α∩4e.␈α∪ While␈α∩executing␈α∪step␈α∩4e,
␈↓ α,␈↓wherever␈α
a␈αsubstitution␈α
in␈αthe␈α
left␈α
field␈αis␈α
made,␈αthe␈α
entry␈α
is␈αrehashed␈α
according␈αto␈α
the␈α
new␈αleft
␈↓ α,␈↓field␈αcontents␈αand␈αentered␈αin␈αthe␈αappropriate␈αhash␈αchain.␈α The␈αlatter␈αeliminates␈αthe␈αneed␈αfor␈αstep
␈↓ α,␈↓5␈αsince␈α
the␈αact␈α
of␈αentering␈α
the␈αitem␈α
in␈αthe␈α
new␈αhash␈α
bucket␈αalso␈α
includes␈αa␈α
check␈αof␈α
its␈αpresence␈α
in
␈↓ α,␈↓the␈α∂chain.␈α∂ In␈α∂fact,␈α∞we␈α∂can␈α∂now␈α∂slightly␈α∞modify␈α∂the␈α∂updating␈α∂algorithm␈α∞to␈α∂keep␈α∂a␈α∂list␈α∂of␈α∞items
␈↓ α,␈↓having␈αidentical␈αcontents␈αthat␈αhave␈αnot␈αyet␈αbeen␈αmerged.␈α Actually,␈αthis␈αis␈αthe␈αsame␈αas␈αmods␈αonly
␈↓ α,␈↓now␈αwe␈αknow␈αexactly␈αwhich␈αentries␈αare␈αidentical␈αwhere␈αpreviously␈αthis␈αwas␈αascertained␈αby␈αmeans
␈↓ α,␈↓of␈αstep␈α5.␈α
 No␈αmodifications␈αare␈α
proposed␈αto␈αstep␈α4c␈α
which␈αchecks␈αif␈α
the␈αproposed␈αmerge␈αof␈α
classes
␈↓ α,␈↓will␈α∩result␈α⊃in␈α∩a␈α∩contradiction.␈α⊃ Moreover,␈α∩we␈α⊃use␈α∩a␈α∩count␈α⊃pointer␈α∩to␈α⊃indicate␈α∩the␈α∩number␈α⊃of
␈↓ α,␈↓arguments␈α∂by␈α∞the␈α∂left(table)␈α∂entry␈α∞where␈α∂atoms␈α∞are␈α∂represented␈α∂as␈α∞functions␈α∂of␈α∂zero␈α∞arguments.
␈↓ α,␈↓The␈α
latter␈α∞also␈α
acts␈α
as␈α∞a␈α
filter␈α
when␈α∞collisions␈α
occur␈α
in␈α∞the␈α
hash␈α
table␈α∞since␈α
equality␈α∞checks␈α
will
␈↓ α,␈↓only␈α⊃need␈α∩to␈α⊃be␈α⊃performed␈α∩when␈α⊃both␈α⊃the␈α∩hashed␈α⊃value␈α⊃and␈α∩the␈α⊃number␈α⊃of␈α∩arguments␈α⊃are
␈↓ α,␈↓identical.

␈↓ α,␈↓Therefore␈α∃we␈α∃have␈α∀seen␈α∃that␈α∃our␈α∀equality␈α∃determination␈α∃and␈α∀updating␈α∃algorithms␈α∃can␈α∀be
␈↓ α,␈↓implemented␈α⊂in␈α⊂a␈α⊂manner␈α⊃which␈α⊂is␈α⊂largely␈α⊂dependent␈α⊂on␈α⊃the␈α⊂speed␈α⊂with␈α⊂which␈α⊂items␈α⊃can␈α⊂be
␈↓ α,␈↓looked␈α∂up␈α∂in␈α∂a␈α∂hashed␈α∂table.␈α∂ Furthermore,␈α∞the␈α∂equality␈α∂determination␈α∂algorithm␈α∂is␈α∂seen␈α∂to␈α∞be
␈↓ α,␈↓almost␈α∂linear,␈α∂on␈α∂the␈α∞average,␈α∂in␈α∂the␈α∂sense␈α∞that␈α∂the␈α∂time␈α∂necessary␈α∞to␈α∂decide␈α∂if␈α∂two␈α∂strings␈α∞are
␈↓ α,␈↓identical␈α⊃is␈α⊃proprtional␈α⊃to␈α⊃the␈α⊃length␈α⊃of␈α⊂the␈α⊃two␈α⊃strings.␈α⊃ Moreover,␈α⊃we␈α⊃have␈α⊃devised␈α⊃a␈α⊂data
␈↓ α,␈↓structure␈αwhich␈α
allows␈αthe␈α
updating␈αof␈α
the␈αdata␈α
base␈αwithout␈α
performing␈αuseless␈α
operations␈α(this
␈↓ α,␈↓includes␈αthe␈αmany␈αpasses␈αover␈αthe␈αdata␈αbase␈αthat␈αthe␈αalgorithm␈αin␈αFigure␈α6␈αmight␈αpossibly␈αmake).
␈↓ α,␈↓As␈αa␈αfinal␈αobservation␈αwe␈αnote␈αthat␈αprevious␈αstipulations␈αthat␈αall␈αdata␈αbase␈αentries␈αrefer␈α
to␈αlower
␈↓ α,␈↓numbered␈αequivalence␈αclasses␈αis␈αno␈αlonger␈αnecessary.␈α The␈αreason␈αthis␈αrequirement␈αwas␈αmade␈αwas
␈↓ α,␈↓to enable us to avoid searching the entire table in steps 4d and 4e of the algorithm in Figure 6.




















␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:19␈↓ ,



␈↓ α,␈↓___________________________________________________________________________________________
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α+pointer to head of the␈↓ π≤|              pointer to next entry␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α∞equivalence class␈↓ π≤|          having the same hash value␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈αfirst table entry having the␈↓ π≤|           pointer to next table entry␈↓ ≤|
␈↓ α,␈↓|␈α:equivalence class name as an argument␈↓ π≤|          in the same equivalence class␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈α?␈α=function name or atom name␈↓ π≤|             number of arguments␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|           pointer to next equivalence␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α1argument 1␈↓ π≤|            class in which argument 1␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|              occurs as an argument␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|           pointer to next equivalence␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α1argument 2␈↓ π≤|            class in which argument 2␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|              occurs as an argument␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α?␈α9.␈↓ π≤|                      .␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α?␈α9.␈↓ π≤|                      .␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α?␈α9.␈↓ π≤|                      .␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|
␈↓ α,␈↓|␈↓ π≤|␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|           pointer to next equivalence␈↓ ≤|
␈↓ α,␈↓|␈α?␈α?␈α?␈α-argument m␈↓ π≤|            class in which argument m␈↓ ≤|
␈↓ α,␈↓|␈↓ π≤|              occurs as an argument␈↓ ≤|
␈↓ α,␈↓|____________________________________________|_____________________________________________|



␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α∩Figure 7













␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:20␈↓ ,



␈↓ α,␈↓VIII.  CONCLUSION AND FUTURE WORK

␈↓ α,␈↓At␈αthis␈αpoint␈αwe␈αmention␈αthat␈αwe␈αhave␈αsucceeded␈αin␈αanswering␈αthe␈αoriginal␈αset␈αof␈αquestions␈αposed
␈↓ α,␈↓in␈αthe␈αintroduction.␈α Moreover,␈αthe␈αorder␈αin␈αwhich␈αequality␈αpairs␈αare␈αadded␈αto␈αthe␈αdata␈αbase␈αhas
␈↓ α,␈↓no␈αbearing␈αon␈αthe␈αactual␈αprocess␈αof␈α
checking␈αequality␈αsince␈αeach␈αcomputation␈αis␈αin␈αan␈α
equivalence
␈↓ α,␈↓class␈α∪and␈α∪at␈α∪each␈α∀point␈α∪all␈α∪possible␈α∪equivalences␈α∪are␈α∀taken␈α∪advantage␈α∪of␈α∪as␈α∪shown␈α∀in␈α∪the
␈↓ α,␈↓algorithms and their proofs.

␈↓ α,␈↓Some␈α∪directions␈α∪for␈α∀future␈α∪work␈α∪include␈α∪the␈α∀ability␈α∪to␈α∪handle␈α∪commutative␈α∀and␈α∪associative
␈↓ α,␈↓functions,␈α∞transitvity␈α∞of␈α∞functions,␈α
and␈α∞certain␈α∞relations␈α∞of␈α
equality␈α∞for␈α∞functions.␈α∞ This␈α
includes
␈↓ α,␈↓such␈α/examples␈α/as␈α/ CONS(A,B)=XCONS(B,A)␈α/,␈α/LESSP(A,B)=GREATERP(B,A)␈α/,
␈↓ α,␈↓CAR(CONS(A,B))=A␈α,␈αetc.␈α These␈αrelations␈αwould␈αbe␈αhandled␈αon␈αan␈αinstance␈αbasis␈αand␈αnot␈αon␈αa
␈↓ α,␈↓general␈α∂variable␈α∞basis.␈α∂ This␈α∞means␈α∂that␈α∞when␈α∂certain␈α∞functions␈α∂are␈α∞encountered,␈α∂equalities␈α∞are
␈↓ α,␈↓added␈α⊂to␈α⊂the␈α⊂data␈α⊂base.␈α∂ Such␈α⊂a␈α⊂scheme␈α⊂could␈α⊂adequately␈α∂deal␈α⊂with␈α⊂quite␈α⊂a␈α⊂large␈α⊂number␈α∂of
␈↓ α,␈↓known␈α∪relationships␈α∀between␈α∪functions.␈α∪ However,␈α∀we␈α∪would␈α∀still␈α∪not␈α∪be␈α∀able␈α∪to␈α∀cope␈α∪with
␈↓ α,␈↓examples␈α
such␈α
as␈αf(x)=x␈α
where␈α
x␈α
is␈αa␈α
free␈α
variable␈α
(i.e.␈αnot␈α
an␈α
instance).␈α
 In␈αfact␈α
such␈α
a␈αsystem␈α
will
␈↓ α,␈↓only␈α∞treat␈α∞equality␈α∞between␈α
functions,␈α∞and␈α∞not␈α∞equality␈α
between␈α∞functions␈α∞and␈α∞variables.␈α
 When
␈↓ α,␈↓these␈α
extensions␈α
are␈α
made,␈α
the␈α
proof␈α
of␈α
the␈α
algorithm␈α
will␈α
have␈α
to␈α
be␈α
modified␈α
to␈α
read␈α
"equality␈α
of
␈↓ α,␈↓two items will be determined subject to its being derivable from the known set of equalities".






























␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:21␈↓ ,



␈↓ α,␈↓APPENDIX

␈↓ α,␈↓Precedence␈αrelations␈αfor␈α
a␈αgrammar␈αG=(V,T,P,S)␈αare␈α
defined␈αas␈αfollows:␈α (x,␈α
y,␈αand␈αz␈αare␈α
arbitrary
␈↓ α,␈↓strings of length zero or more over the vocabulary and Bi represents element i of the vocabulary)

␈↓ α,␈↓Bi = Bj  iff ∃ k  such that  Bk →→ x Bi Bj y 

␈↓ α,␈↓Bi < Bj  iff ∃ k  such that  Bi = Bk  and  Bk *→→ Bj x 

␈↓ α,␈↓Bi > Bj  iff ∃ k  such that  Bk *→→ x Bi  and  Bk = Bj  
␈↓ α,␈↓         or ∃ m,n such that  Bm = Bn  and  Bm *→→ y Bi  and  Bn *→→ Bj z 

␈↓ α,␈↓A grammar is said to be simple precedence if:

␈↓ α,␈↓1.  No two productions have the same right hand part.

␈↓ α,␈↓2.␈α At␈αmost␈αone␈αof␈αthe␈αthree␈αprecedence␈αrelations␈α=,␈α<,␈αand␈α>␈αhold␈αbetween␈αany␈αtwo␈αsymbols␈αof␈α
the
␈↓ α,␈↓vocabulary

␈↓ α,␈↓␈↓&Theorem:␈↓'β  GE is always simple precedence

␈↓ α,␈↓␈↓&Proof:␈↓'β␈α We␈αfirst␈αshow␈αthat␈αat␈αmost␈αone␈αprecedence␈αrelation␈αmay␈αhold␈αbetween␈αany␈αtwo␈αsymbols␈αof
␈↓ α,␈↓the vocabulary.

␈↓ α,␈↓1.␈α
 a␈α
<␈α
b␈α
 implies␈α
that␈α
b␈α
is␈α
a␈α
leftmost␈αsymbol␈α
of␈α
some␈α
production.␈α
 Therefore␈α
b␈α
is␈α
an␈α
atom␈α
or␈α"(".␈α
 a
␈↓ α,␈↓=␈α
b␈α
 implies␈α
that␈α
b␈αappears␈α
adjacent␈α
to␈α
the␈α
right␈αof␈α
a.␈α
 However,␈α
b␈α
is␈αan␈α
atom␈α
or␈α
"("␈α
neither␈αof
␈↓ α,␈↓which␈α∞can␈α∞ever␈α∞appear␈α∞adjacent␈α∞to␈α∞the␈α∞right␈α∞of␈α∞any␈α∞symbol.␈α∞ Therefore␈α∞ a␈α∞<␈α∞b␈α∞ and␈α∞ a␈α∞=␈α∞b␈α∞ is
␈↓ α,␈↓impossible.

␈↓ α,␈↓2.␈α a␈α>␈αb␈α implies␈αthat␈αa␈αis␈αa␈αrightmost␈αsymbol␈αof␈αsome␈αproduction.␈α Therefore␈αa␈αis␈αan␈αatom␈αor␈α
")".
␈↓ α,␈↓a␈α
=␈αb␈α
 implies␈α
that␈αa␈α
appears␈αadjacent␈α
to␈α
the␈αleft␈α
of␈α
b.␈α However,␈α
a␈αis␈α
an␈α
atom␈αor␈α
")"␈α
neither␈αof
␈↓ α,␈↓which␈α∂can␈α∂ever␈α∂appear␈α∂adjacent␈α∂to␈α⊂the␈α∂left␈α∂of␈α∂any␈α∂symbol.␈α∂ Therefore␈α⊂ a␈α∂>␈α∂b␈α∂ and␈α∂ a␈α∂=␈α⊂b␈α∂ is
␈↓ α,␈↓impossible.

␈↓ α,␈↓3.␈α a␈α>␈αb␈αimplies␈αthat␈αa␈αis␈αa␈αrightmost␈αsymbol␈αof␈αsome␈αproduction.␈α Therefore␈αa␈αis␈αan␈αatom␈αor␈α")".
␈↓ α,␈↓a␈α<␈αb␈α implies␈α that␈αthere␈α
exists␈αa␈αnonterminal␈αC␈αsuch␈αthat␈α
 a␈α=␈αC␈α.␈α However,␈αthis␈α
is␈αimpossible
␈↓ α,␈↓since␈α
no␈α
symbol␈αcan␈α
ever␈α
appear␈αadjacent␈α
to␈α
the␈αright␈α
of␈α
an␈α
atom␈αor␈α
"(".␈α
 Therefore␈α a␈α
>␈α
b␈α and␈α
 a
␈↓ α,␈↓< b  is impossible.

␈↓ α,␈↓Thus␈α∩we␈α∩have␈α∩shown␈α∩that␈α∩our␈α∩grammar,␈α∩GE,␈α∩always␈α∩satisfies␈α∩the␈α∩criteria␈α∩that␈α∩at␈α∪most␈α∩one
␈↓ α,␈↓precedence␈α∪relation␈α∪ever␈α∪holds␈α∪between␈α∪any␈α∪two␈α∪symbols␈α∪of␈α∪the␈α∪vocabulary.␈α∀ Moreover,␈α∪the
␈↓ α,␈↓updating␈α∞algorithm␈α∂preserves␈α∞the␈α∂uniqueness␈α∞of␈α∞right␈α∂hand␈α∞sides␈α∂of␈α∞productions,␈α∂and␈α∞therefore
␈↓ α,␈↓regardless of the additional equality pairs the equality grammar, GE, is always simple precedence.






␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:22␈↓ ,



␈↓ α,␈↓REFERENCES

␈↓ α,␈↓[1]  McCarthy, J., LISP 1.5 Programmer's manual


␈↓ α,␈↓[2]  Allen, J., Interactive Theorem Prover


␈↓ α,␈↓[3]␈α∪ Martin,␈α∪D.,␈α∀Algorithms␈α∪for␈α∪Generation␈α∪of␈α∀Boolean␈α∪Matrices␈α∪for␈α∀Computing␈α∪Precedence
␈↓ α,␈↓Relations







































␈↓ α,␈↓␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α?␈α:23␈↓ ,